let x be object ; :: thesis: for L being Z_Lattice
for L1, L2 being Z_Sublattice of L st x in L1 & L1 is Z_Sublattice of L2 holds
x in L2
let L be Z_Lattice; :: thesis: for L1, L2 being Z_Sublattice of L st x in L1 & L1 is Z_Sublattice of L2 holds
x in L2
let L1, L2 be Z_Sublattice of L; :: thesis: ( x in L1 & L1 is Z_Sublattice of L2 implies x in L2 )
assume AS: ( x in L1 & L1 is Z_Sublattice of L2 ) ; :: thesis: x in L2
then A1: L1 is Submodule of L2 by ThSL1;
( L1 is Submodule of L & L2 is Submodule of L ) by ThSL1;
hence x in L2 by AS, A1, ZMODUL01:23; :: thesis: verum