theorem :: ZMODLAT1:22

for x being object
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