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