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 T0: 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 p' = p, q' = q as Element of L by T0;

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 p' "\/" q' = q' by T0;
then p' [= q' 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 p' [= q' by FILTER_1:32;
then p' "\/" q' = q' by LATTICES:def 3;
then p "\/" q = q by T0;
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 T0, RELSET_1:def 3; :: thesis: verum