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 .:) = { [p9,q9] where p9, q9 is Element of (L .:) : p9 [= q9 } 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 object ; :: 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 p9 = p, q9 = q as Element of (L .:) by A3;
A6: x = q by A4, XTUPLE_0:1;
A7: y = p by A4, XTUPLE_0:1;
q9 [= p9 by A5, LATTICE2:38;
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 p9, q9 being Element of (L .:) such that
A8: [x,y] = [p9,q9] and
A9: p9 [= q9 by A2;
reconsider p = p9, q = q9 as Element of L by A3;
A10: x = p by A8, XTUPLE_0:1;
A11: y = q by A8, XTUPLE_0:1;
q [= p by A9, LATTICE2:39;
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