let L be lower-bounded sup-Semilattice; :: thesis: IdsMap L in the carrier of (MonSet L)
set s = IdsMap L;
ex s' being Function of L,(InclPoset (Ids L)) st
( IdsMap L = s' & s' is monotone & ( for x being Element of L holds s' . 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 Def14; :: thesis: verum