let K, L be Lattice; ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) implies LattPOSet K = LattPOSet L )
assume A1:
LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #)
; LattPOSet K = LattPOSet L
for p, q being Element of K holds
( [p,q] in LattRel K iff [p,q] in LattRel L )
hence
LattPOSet K = LattPOSet L
by A1, RELSET_1:def 2; verum