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:24;
then ( Rel2Map L is one-to-one & rng (Rel2Map L) = dom (Map2Rel L) & (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) ) by Th30, Th31, FUNCT_2:def 1;
hence (Rel2Map L) " = Map2Rel L by FUNCT_1:63; :: thesis: verum