let L be Z_Lattice; :: thesis: 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 () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let A be non empty set ; :: thesis: 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 () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ze be Element of A; :: thesis: 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 () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ad be BinOp of A; :: thesis: 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 () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let mu be Function of [: the carrier of INT.Ring,A:],A; :: thesis: for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] holds
LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let sc be Function of [:A,A:], the carrier of F_Real; :: thesis: ( A is linearly-closed Subset of () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] implies LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L )
assume A1: ( A is linearly-closed Subset of () & ze = 0. () & ad = the addF of () || A & mu = the lmult of () | [: the carrier of INT.Ring,A:] ) ; :: thesis: LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L
set L1 = LatticeStr(# A,ad,ze,mu,sc #);
set V1 = ModuleStr(# A,ad,ze,mu #);
A2: ModuleStr(# A,ad,ze,mu #) is Submodule of DivisibleMod L by ;
reconsider V1 = ModuleStr(# A,ad,ze,mu #) as Z_Module by ;
reconsider scc = sc as Function of [: the carrier of V1, the carrier of V1:], the carrier of F_Real ;
LatticeStr(# A,ad,ze,mu,sc #) = GenLat (V1,scc) ;
then LatticeStr(# A,ad,ze,mu,sc #) is Submodule of V1 by ZMODLAT1:2;
hence LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L by ; :: thesis: verum