theorem Th30: :: WAYBEL_4:30

for L being lower-bounded sup-Semilattice holds (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))