let K, L be Lattice; :: thesis: ( 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 #) ; :: thesis: LattPOSet K = LattPOSet L
for p, q being Element of K holds
( [p,q] in LattRel K iff [p,q] in LattRel L )

proof

let p, q be Element of K; :: thesis: ( [p,q] in LattRel K iff [p,q] in LattRel L )
reconsider p9 = p, q9 = q as Element of L by A1;

hereby :: thesis: ( [p,q] in LattRel L implies [p,q] in LattRel K )

assume [p,q] in LattRel K ; :: thesis: [p,q] in LattRel L
then p [= q by FILTER_1:32;
then p "\/" q = q by LATTICES:def 3;
then p9 "\/" q9 = q9 by A1;
then p9 [= q9 by LATTICES:def 3;
hence [p,q] in LattRel L by FILTER_1:32; :: thesis: verum

end;

assume [p,q] in LattRel L ; :: thesis: [p,q] in LattRel K
then p9 [= q9 by FILTER_1:32;
then p9 "\/" q9 = q9 by LATTICES:def 3;
then p "\/" q = q by A1;
then p [= q by LATTICES:def 3;
hence [p,q] in LattRel K by FILTER_1:32; :: thesis: verum

end;

hence LattPOSet K = LattPOSet L by A1, RELSET_1:def 3; :: thesis: verum