let L be Z_Lattice; :: thesis: for L1, L2 being Z_Sublattice of L holds 0. L1 in L2
let L1, L2 be Z_Sublattice of L; :: thesis: 0. L1 in L2
( L1 is Submodule of L & L2 is Submodule of L ) by ThSL1;
hence 0. L1 in L2 by ZMODUL01:34; :: thesis: verum