theorem Th6: :: LATTICE3:6
for L1, L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds
LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #)