let L be Lattice; :: thesis: ( () ~ = LattRel (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 .:) :: thesis: () ~ = LattPOSet (L .:)
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in () ~ or [x,y] in LattRel (L .:) ) & ( not [x,y] in LattRel (L .:) or [x,y] in () ~ ) )
thus ( [x,y] in () ~ implies [x,y] in LattRel (L .:) ) :: thesis: ( not [x,y] in LattRel (L .:) or [x,y] in () ~ )
proof
assume [x,y] in () ~ ; :: 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 ;
A7: y = p by ;
q9 [= p9 by ;
hence [x,y] in LattRel (L .:) by A2, A6, A7; :: thesis: verum
end;
assume [x,y] in LattRel (L .:) ; :: thesis: [x,y] in () ~
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 ;
A11: y = q by ;
q [= p by ;
then [y,x] in LattRel L by A1, A10, A11;
hence [x,y] in () ~ by RELAT_1:def 7; :: thesis: verum
end;
hence (LattPOSet L) ~ = LattPOSet (L .:) by A3; :: thesis: verum