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

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