let L be lower-bounded sup-Semilattice; :: thesis: (Rel2Map L) " = Map2Rel L
( (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) implies rng (Rel2Map L) = the carrier of (MonSet L) ) by FUNCT_2:18;
then A1: rng (Rel2Map L) = dom (Map2Rel L) by Th31, FUNCT_2:def 1;
(Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by Th30;
hence (Rel2Map L) " = Map2Rel L by A1, FUNCT_1:41; :: thesis: verum