for L being Z_Lattice
for A being non empty set
for ze being Element of A
for ad being BinOp of A
for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L