Every subgroup of a free discrete group is free.
Nielsen’s theorem is the weaker form proved by J. Nielsen in 1921 saying that every finitely generated subgroup of a free group is free. Otto Schreier proved in 1927 the theorem in full generality.
The algebraic proof of this theorem is rather long and complicated and it is usually based on Nielsen’s method of short cancellations in combinatorial group theory based on words (Nielsen’s transformations of words, word length functions, …). The class of projective group?s (projective objects in the category of groups) coincides with the class of free groups.
There is however a short proof by the basic methods of algebraic topology.
As stated, the theorem is not valid in constructive mathematics, although Nielsen's weaker 1921 version is.
W. Magnus, A. Karras, D. Solitar, Combinatorial group theory
R. Lindon, P. Schupp, Combinatorial group theory, Springer 1977 (Russian transl. Mir, Moskva 1980)
O. Schreier, Die Untergruppen der freien Gruppen, Abh. Mat Sem. Univ. Hamburg 3, 167–169, 1927.
H. Zieschang, Über die Nielsensche Kürzungsmethods in freien Produkten mit Amalgam, Invent. Math. 10, 4–37, 1970.