let L be lower-bounded sup-Semilattice; :: thesis: (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 ; :: thesis: ( a in Aux L implies ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a )
assume A3: a in Aux L ; :: thesis: ((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 ; :: thesis: ( [c,b] in La iff [c,b] in AR )

hereby :: thesis: ( [c,b] in AR implies [c,b] in La )

assume A8: [c,b] in La ; :: thesis: [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; :: thesis: verum

end;

assume A13: [c,b] in AR ; :: thesis: [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; :: thesis: verum

end;

then La = AR ;
hence ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a by A5, FUNCT_1:18; :: thesis: verum

end;

hence (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by A1, A2, FUNCT_1:2; :: thesis: verum