let L be Semilattice; :: thesis: for I being Ideal of L holds DownMap I in the carrier of (MonSet L)
let I be Ideal of L; :: thesis: DownMap I in the carrier of (MonSet L)
reconsider mI = DownMap I as Function of L,(InclPoset (Ids L)) ;
ex s being Function of L,(InclPoset (Ids L)) st
( mI = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )

proof

take mI ; :: thesis: ( mI = mI & mI is monotone & ( for x being Element of L holds mI . x c= downarrow x ) )
thus ( mI = mI & mI is monotone & ( for x being Element of L holds mI . x c= downarrow x ) ) by Lm9, Lm10; :: thesis: verum

end;

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