let L be lower-bounded sup-Semilattice; :: thesis: (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
set LS = (Rel2Map L) * (Map2Rel L);
set R = id the carrier of (MonSet L);
A1: dom ((Rel2Map L) * (Map2Rel L)) = the carrier of (MonSet L) by FUNCT_2:def 1;
A2: dom (id the carrier of (MonSet L)) = the carrier of (MonSet L) ;
for a being object st a in the carrier of (MonSet L) holds
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a

proof

let a be object ; :: thesis: ( a in the carrier of (MonSet L) implies ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a )
assume A3: a in the carrier of (MonSet L) ; :: thesis: ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
then consider s being Function of L,(InclPoset (Ids L)) such that
A4: a = s and
s is monotone and
for x being Element of L holds s . x c= downarrow x by Def13;
((Rel2Map L) * (Map2Rel L)) . s in the carrier of (MonSet L) by A3, A4, FUNCT_2:5;
then consider Ls being Function of L,(InclPoset (Ids L)) such that
A5: ((Rel2Map L) * (Map2Rel L)) . s = Ls and
Ls is monotone and
for x being Element of L holds Ls . x c= downarrow x by Def13;
set AR = (Map2Rel L) . s;
(Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A3, A4, FUNCT_2:5;
then (Map2Rel L) . s in Aux L by YELLOW_1:1;
then reconsider AR = (Map2Rel L) . s as auxiliary Relation of L by Def8;
dom (Map2Rel L) = the carrier of (MonSet L) by FUNCT_2:def 1;
then Ls = (Rel2Map L) . AR by A3, A4, A5, FUNCT_1:13;
then A6: Ls = AR -below by Def14;
A7: dom Ls = the carrier of L by FUNCT_2:def 1;
A8: dom s = the carrier of L by FUNCT_2:def 1;

now :: thesis: for b being object st b in the carrier of L holds
Ls . b = s . b

let b be object ; :: thesis: ( b in the carrier of L implies Ls . b = s . b )
assume A9: b in the carrier of L ; :: thesis: Ls . b = s . b
then reconsider b9 = b as Element of L ;
A10: Ls . b c= s . b

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in Ls . b or d in s . b )
assume d in Ls . b ; :: thesis: d in s . b
then d in AR -below b9 by A6, Def12;
then A11: [d,b9] in AR by Th13;
ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . s & ( for d, b9 being object holds
( [d,b9] in AR9 iff ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) ) ) ) by A3, A4, Def15;
then ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) by A11;
hence d in s . b ; :: thesis: verum

end;

s . b c= Ls . b

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in s . b or d in Ls . b )
assume A12: d in s . b ; :: thesis: d in Ls . b
s . b in the carrier of (InclPoset (Ids L)) by A9, FUNCT_2:5;
then s . b in Ids L by YELLOW_1:1;
then ex X being Ideal of L st s . b = X ;
then reconsider d9 = d as Element of L by A12;
ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . s & ( for d, b9 being object holds
( [d,b9] in AR9 iff ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) ) ) ) by A3, A4, Def15;
then [d9,b9] in AR by A12;
then d9 in AR -below b9 ;
hence d in Ls . b by A6, Def12; :: thesis: verum

end;

hence Ls . b = s . b by A10; :: thesis: verum

end;

then Ls = s by A7, A8, FUNCT_1:2;
hence ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a by A3, A4, A5, FUNCT_1:18; :: thesis: verum

end;

hence (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) by A1, A2, FUNCT_1:2; :: thesis: verum