let L be Z_Lattice; :: thesis: DualLatMod L is Submodule of DivisibleMod L
( the carrier of (DualLatMod L) = DualSet L & the addF of (DualLatMod L) = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of (DualLatMod L) = 0. (DivisibleMod L) & the lmult of (DualLatMod L) = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of (DualLatMod L) = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) by defDualMod;
hence DualLatMod L is Submodule of DivisibleMod L by ZMODLAT2:10; :: thesis: verum