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

proof

take IdsMap L ; :: thesis: ( IdsMap L = IdsMap L & IdsMap L is monotone & ( for x being Element of L holds (IdsMap L) . x c= downarrow x ) )
thus ( IdsMap L = IdsMap L & IdsMap L is monotone & ( for x being Element of L holds (IdsMap L) . x c= downarrow x ) ) by YELLOW_2:def 4; :: thesis: verum

end;

hence IdsMap L in the carrier of (MonSet L) by Def13; :: thesis: verum