:: deftheorem RL5Def4 defines Submodules_of ZMODUL05:def 1 :
for V being free finite-rank Z_Module
for n being Nat
for b₃ being set holds
( b₃ = n Submodules_of V iff for x being object holds
( x in b₃ iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) );