let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L holds L1 is Submodule of L
let L1 be Z_Sublattice of L; :: thesis: L1 is Submodule of L
A1: the carrier of L1 c= the carrier of L by defSublattice;
A2: the addF of L1 = the addF of L || the carrier of L1 by defSublattice;
A3: 0. L1 = 0. L by defSublattice;
the lmult of L1 = the lmult of L | [: the carrier of INT.Ring, the carrier of L1:] by defSublattice;
hence L1 is Submodule of L by A1, A2, A3, VECTSP_4:def 2; :: thesis: verum