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 )

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

hence
LattPOSet K = LattPOSet L
by A1, RELSET_1:def 2; :: thesis: verum
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;

then p9 [= q9 by FILTER_1:31;

then p9 "\/" q9 = q9 ;

then p "\/" q = q by A1;

then p [= q ;

hence [p,q] in LattRel K by FILTER_1:31; :: thesis: verum

end;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 L
; :: thesis: [p,q] in LattRel Kassume
[p,q] in LattRel K
; :: thesis: [p,q] in LattRel L

then p [= q by FILTER_1:31;

then p "\/" q = q ;

then p9 "\/" q9 = q9 by A1;

then p9 [= q9 ;

hence [p,q] in LattRel L by FILTER_1:31; :: thesis: verum

end;then p [= q by FILTER_1:31;

then p "\/" q = q ;

then p9 "\/" q9 = q9 by A1;

then p9 [= q9 ;

hence [p,q] in LattRel L by FILTER_1:31; :: thesis: verum

then p9 [= q9 by FILTER_1:31;

then p9 "\/" q9 = q9 ;

then p "\/" q = q by A1;

then p [= q ;

hence [p,q] in LattRel K by FILTER_1:31; :: thesis: verum