let V be free finite-rank Z_Module; :: thesis: for n being Nat st n <= rank V holds
not n Submodules_of V is empty
let n be Nat; :: thesis: ( n <= rank V implies not n Submodules_of V is empty )
assume n <= rank V ; :: thesis: not n Submodules_of V is empty
then ex W being strict free Submodule of V st rank W = n by RL5Lm2;
hence not n Submodules_of V is empty by RL5Def4; :: thesis: verum