let L be lower-bounded sup-Semilattice; :: thesis: the carrier of L --> {(Bottom L)} in the carrier of (MonSet L)
set s = the carrier of L --> {(Bottom L)};
ex s9 being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = s9 & s9 is monotone & ( for x being Element of L holds s9 . x c= downarrow x ) )

proof

reconsider s = the carrier of L --> {(Bottom L)} as Function of L,(InclPoset (Ids L)) by Th25;
take s ; :: thesis: ( the carrier of L --> {(Bottom L)} = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )
for x being Element of L holds s . x c= downarrow x by Lm4;
hence ( the carrier of L --> {(Bottom L)} = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by Lm5; :: thesis: verum

end;

hence the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) by Def13; :: thesis: verum