:: deftheorem defines LC_Z_Module ZMODUL02:def 35 :
for V being Z_Module
for A being Subset of V
for b₃ being strict Submodule of LC_Z_Module V holds
( b₃ = LC_Z_Module A iff the carrier of b₃ = { l where l is Linear_Combination of A : verum } );