let V be free finite-rank Z_Module; :: thesis: for n being Nat st rank V < n holds
n Submodules_of V = {}
let n be Nat; :: thesis: ( rank V < n implies n Submodules_of V = {} )
assume that
A1: rank V < n and
A2: n Submodules_of V <> {} ; :: thesis: contradiction
consider x being object such that
A3: x in n Submodules_of V by A2, XBOOLE_0:def 1;
ex W being strict free Submodule of V st
( W = x & rank W = n ) by A3, RL5Def4;
hence contradiction by A1, RL5Th29; :: thesis: verum