for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds
( n <= rank V iff ex W being strict free Submodule of V st rank W = n ) by RL5Lm2, RL5Th29;