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;