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 } & LattRel (L .: ) = { [p',q'] where p', q' is Element of (L .: ) : p' [= q' } & L .: = LattStr(# H1(L),H3(L),H2(L) #) & LattStr(# the carrier of L,the L_join of L,the L_meet of L #) = LattStr(# H1(L),H2(L),H3(L) #) )
by FILTER_1:def 8, 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 A2:
(
[y,x] = [p,q] &
p [= q )
by A1;
reconsider p' =
p,
q' =
q as
Element of
(L .: ) by A1;
(
x = q &
y = p &
q' [= p' )
by A2, LATTICE2:53, ZFMISC_1:33;
hence
[x,y] in LattRel (L .: )
by A1;
:: 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 A3:
(
[x,y] = [p',q'] &
p' [= q' )
by A1;
reconsider p =
p',
q =
q' as
Element of
L by A1;
(
x = p &
y = q &
q [= p )
by A3, LATTICE2:54, ZFMISC_1:33;
then
[y,x] in LattRel L
by A1;
hence
[x,y] in (LattRel L) ~
by RELAT_1:def 7;
:: thesis: verum
end;
hence
(LattPOSet L) ~ = LattPOSet (L .: )
by A1; :: thesis: verum