let L be lower-bounded sup-Semilattice; :: thesis: Rel2Map L is isomorphic
ex g being Function of (MonSet L),(InclPoset (Aux L)) st
( g = (Rel2Map L) " & g is monotone )
proof
reconsider g = Map2Rel L as Function of (MonSet L),(InclPoset (Aux L)) ;
take g ; :: thesis: ( g = (Rel2Map L) " & g is monotone )
thus ( g = (Rel2Map L) " & g is monotone ) by Th32; :: thesis: verum
end;
hence Rel2Map L is isomorphic by WAYBEL_0:def 38; :: thesis: verum