let L be Semilattice; :: thesis: for x being Element of L
for I being Ideal of L holds (DownMap I) . x c= downarrow x
let x be Element of L; :: thesis: for I being Ideal of L holds (DownMap I) . x c= downarrow x
let I be Ideal of L; :: thesis: (DownMap I) . x c= downarrow x

per cases ( x <= sup I or not x <= sup I ) ;

suppose x <= sup I ; :: thesis: (DownMap I) . x c= downarrow x

then (DownMap I) . x = (downarrow x) /\ I by Def16;
hence (DownMap I) . x c= downarrow x by XBOOLE_1:17; :: thesis: verum

end;

suppose not x <= sup I ; :: thesis: (DownMap I) . x c= downarrow x

hence (DownMap I) . x c= downarrow x by Def16; :: thesis: verum

end;

end;