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