let L be lower-bounded sup-Semilattice; (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
set LS = (Map2Rel L) * (Rel2Map L);
set R = id (dom (Rel2Map L));
dom ((Map2Rel L) * (Rel2Map L)) = the carrier of (InclPoset (Aux L))
by FUNCT_2:def 1;
then A1:
dom ((Map2Rel L) * (Rel2Map L)) = Aux L
by YELLOW_1:1;
dom (id (dom (Rel2Map L))) = the carrier of (InclPoset (Aux L))
by FUNCT_2:def 1;
then A2:
dom (id (dom (Rel2Map L))) = Aux L
by YELLOW_1:1;
for a being object st a in Aux L holds
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
proof
let a be
object ;
( a in Aux L implies ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a )
assume A3:
a in Aux L
;
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
then reconsider AR =
a as
auxiliary Relation of
L by Def8;
A4:
a in the
carrier of
(InclPoset (Aux L))
by A3, YELLOW_1:1;
then A5:
a in dom (Rel2Map L)
by FUNCT_2:def 1;
then
((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . ((Rel2Map L) . AR)
by FUNCT_1:13;
then A6:
((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . (AR -below)
by Def14;
((Map2Rel L) * (Rel2Map L)) . a in the
carrier of
(InclPoset (Aux L))
by A4, FUNCT_2:5;
then
((Map2Rel L) * (Rel2Map L)) . a in Aux L
by YELLOW_1:1;
then reconsider La =
((Map2Rel L) * (Rel2Map L)) . a as
auxiliary Relation of
L by Def8;
A7:
AR -below in the
carrier of
(MonSet L)
by Th18;
for
c,
b being
object holds
(
[c,b] in La iff
[c,b] in AR )
proof
let c,
b be
object ;
( [c,b] in La iff [c,b] in AR )
hereby ( [c,b] in AR implies [c,b] in La )
assume A8:
[c,b] in La
;
[c,b] in AR
ex
AR9 being
auxiliary Relation of
L st
(
AR9 = (Map2Rel L) . (AR -below) & ( for
c,
b being
object holds
(
[c,b] in AR9 iff ex
c9,
b9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
c9 = c &
b9 = b &
s9 = AR -below &
c9 in s9 . b9 ) ) ) )
by A7, Def15;
then consider c9,
b9 being
Element of
L,
s9 being
Function of
L,
(InclPoset (Ids L)) such that A9:
c9 = c
and A10:
b9 = b
and A11:
s9 = AR -below
and A12:
c9 in s9 . b9
by A6, A8;
c9 in AR -below b9
by A11, A12, Def12;
hence
[c,b] in AR
by A9, A10, Th13;
verum
end;
assume A13:
[c,b] in AR
;
[c,b] in La
then reconsider c9 =
c,
b9 =
b as
Element of
L by ZFMISC_1:87;
c9 in AR -below b9
by A13;
then A14:
c9 in (AR -below) . b9
by Def12;
ex
AR9 being
auxiliary Relation of
L st
(
AR9 = (Map2Rel L) . (AR -below) & ( for
c,
b being
object holds
(
[c,b] in AR9 iff ex
c9,
b9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
c9 = c &
b9 = b &
s9 = AR -below &
c9 in s9 . b9 ) ) ) )
by A7, Def15;
hence
[c,b] in La
by A6, A14;
verum
end;
then
La = AR
;
hence
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
by A5, FUNCT_1:18;
verum
end;
hence
(Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
by A1, A2, FUNCT_1:2; verum