let L be lower-bounded sup-Semilattice; :: thesis:
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 ) )

reconsider s = the carrier of L --> {(Bottom L)} as Function of L,(InclPoset (Ids L)) by Th25;
take s ; :: thesis:
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:

end;