Under the stated choice boundary, every subgroup of a free group is free with its nontrivial Schreier generators as a basis

Suppose first that $X$ is finite, or that $X$ is countable with a chosen enumeration. Then reduced words on $X\bigsqcup X^{-1}$ are ordered first by length and then lexicographically, so every nonempty set of reduced words has a shortlex least element. Choose in each right coset of $H$ its least reduced representative. If $u$ is an initial segment of the chosen representative $w$ for the coset $Hw$, and if the coset $Hu$ had a smaller reduced representative $u^{\mathrm{\prime }}$, then replacing the prefix $u$ of $w$ by $u^{\mathrm{\prime }}$ would produce a smaller representative of $Hw$, impossible. Hence the chosen representatives form a Schreier system.

For arbitrary $X$, [L1] lets us well-order the basis. The same shortlex construction as in step 1.1 then produces a Schreier system. In the countable case, the only choice principle visible in the statement is the weaker bookkeeping of [L2], because step 1.1 already gives the representatives canonically once the enumeration is fixed.

Let $\mathcal{T}$ be a Schreier system obtained from step 1.1 or step 2.1. By [L4], its nontrivial Schreier generators generate $H$, and by [L3] they are freely independent. Therefore [L5] makes them a free basis of $H$.