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_{1}(L),H_{3}(L),H_{2}(L) #)
by LATTICE2:def 2;

thus (LattRel L) ~ = LattRel (L .:) :: thesis: (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

thus (LattRel L) ~ = LattRel (L .:) :: thesis: (LattPOSet L) ~ = LattPOSet (L .:)

proof

hence
(LattPOSet L) ~ = LattPOSet (L .:)
by A3; :: thesis: verum
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) ~ )

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;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) ~
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;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

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