theorem Th31: :: WAYBEL_4:31

for L being lower-bounded sup-Semilattice holds (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)