let V be free finite-rank Z_Module; :: thesis: for W being Submodule of V

for n being Nat holds n Submodules_of W c= n Submodules_of V

let W be Submodule of V; :: thesis: for n being Nat holds n Submodules_of W c= n Submodules_of V

let n be Nat; :: thesis: n Submodules_of W c= n Submodules_of V

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in n Submodules_of W or x in n Submodules_of V )

assume x in n Submodules_of W ; :: thesis: x in n Submodules_of V

then consider W1 being strict free Submodule of W such that

A1: W1 = x and

A2: rank W1 = n by RL5Def4;

reconsider W1 = W1 as strict free Submodule of V by ZMODUL01:42;

W1 in n Submodules_of V by A2, RL5Def4;

hence x in n Submodules_of V by A1; :: thesis: verum

for n being Nat holds n Submodules_of W c= n Submodules_of V

let W be Submodule of V; :: thesis: for n being Nat holds n Submodules_of W c= n Submodules_of V

let n be Nat; :: thesis: n Submodules_of W c= n Submodules_of V

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in n Submodules_of W or x in n Submodules_of V )

assume x in n Submodules_of W ; :: thesis: x in n Submodules_of V

then consider W1 being strict free Submodule of W such that

A1: W1 = x and

A2: rank W1 = n by RL5Def4;

reconsider W1 = W1 as strict free Submodule of V by ZMODUL01:42;

W1 in n Submodules_of V by A2, RL5Def4;

hence x in n Submodules_of V by A1; :: thesis: verum