let L be Lattice; :: thesis: ( (LattRel L) ~ = LattRel (L .: ) & (LattPOSet L) ~ = LattPOSet (L .: ) )
A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def 8;
A2: LattRel (L .: ) = { [p',q'] where p', q' is Element of (L .: ) : p' [= q' } by FILTER_1:def 8;
A3: L .: = LattStr(# H₁(L),H₃(L),H₂(L) #) by LATTICE2:def 2;
thus (LattRel L) ~ = LattRel (L .: ) :: thesis: (LattPOSet L) ~ = LattPOSet (L .: )

proof

let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in (LattRel L) ~ or [x,y] in LattRel (L .: ) ) & ( not [x,y] in LattRel (L .: ) or [x,y] in (LattRel L) ~ ) )
thus ( [x,y] in (LattRel L) ~ implies [x,y] in LattRel (L .: ) ) :: thesis: ( not [x,y] in LattRel (L .: ) or [x,y] in (LattRel L) ~ )

proof

assume [x,y] in (LattRel L) ~ ; :: thesis: [x,y] in LattRel (L .: )
then [y,x] in LattRel L by RELAT_1:def 7;
then consider p, q being Element of L such that
A4: [y,x] = [p,q] and
A5: p [= q by A1;
reconsider p' = p, q' = q as Element of (L .: ) by A3;
A6: x = q by A4, ZFMISC_1:33;
A7: y = p by A4, ZFMISC_1:33;
q' [= p' by A5, LATTICE2:53;
hence [x,y] in LattRel (L .: ) by A2, A6, A7; :: thesis: verum

end;

assume [x,y] in LattRel (L .: ) ; :: thesis: [x,y] in (LattRel L) ~
then consider p', q' being Element of (L .: ) such that
A8: [x,y] = [p',q'] and
A9: p' [= q' by A2;
reconsider p = p', q = q' as Element of L by A3;
A10: x = p by A8, ZFMISC_1:33;
A11: y = q by A8, ZFMISC_1:33;
q [= p by A9, LATTICE2:54;
then [y,x] in LattRel L by A1, A10, A11;
hence [x,y] in (LattRel L) ~ by RELAT_1:def 7; :: thesis: verum

end;

hence (LattPOSet L) ~ = LattPOSet (L .: ) by A3; :: thesis: verum