let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L holds 0. L1 in L
let L1 be Z_Sublattice of L; :: thesis: 0. L1 in L
L1 is Submodule of L by ThSL1;
hence 0. L1 in L by ZMODUL01:35; :: thesis: verum