theorem Th6: :: LATWAL_2:30

for L1, L2 being WA_Lattice st LatRelStr L1 = LatRelStr 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 #)