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

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