let L be Lattice; ( (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(# H1(L),H3(L),H2(L) #)
by LATTICE2:def 2;
thus
(LattRel L) ~ = LattRel (L .:)
(LattPOSet L) ~ = LattPOSet (L .:)proof
let x,
y be
object ;
RELAT_1:def 2 ( ( 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 .:) )
( not [x,y] in LattRel (L .:) or [x,y] in (LattRel L) ~ )proof
assume
[x,y] in (LattRel L) ~
;
[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;
verum
end;
assume
[x,y] in LattRel (L .:)
;
[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;
verum
end;
hence
(LattPOSet L) ~ = LattPOSet (L .:)
by A3; verum