let L be Z_Lattice; :: thesis: for L1, L2 being Z_Sublattice of L holds 0. L1 = 0. L2
let L1, L2 be Z_Sublattice of L; :: thesis: 0. L1 = 0. L2
thus 0. L1 = 0. L by defSublattice
.= 0. L2 by defSublattice ; :: thesis: verum