let L be lower-bounded sup-Semilattice; :: thesis: the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L))
{(Bottom L)} = downarrow (Bottom L) by Th23;
then {(Bottom L)} in { X where X is Ideal of L : verum } ;
then {(Bottom L)} in the carrier of (InclPoset (Ids L)) by YELLOW_1:1;
hence the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L)) by FUNCOP_1:45; :: thesis: verum