let L be Semilattice; :: thesis: for I being Ideal of L holds DownMap I is monotone
let I be Ideal of L; :: thesis: DownMap I is monotone
let x, y be Element of L; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ ) )
assume A1: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ )

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

suppose A2: ( x <= sup I & y <= sup I ) ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ )

then A3: (DownMap I) . x = (downarrow x) /\ I by Def16;
(DownMap I) . y = (downarrow y) /\ I by A2, Def16;
then (DownMap I) . x c= (DownMap I) . y by A1, A3, WAYBEL_0:21, XBOOLE_1:26;
hence for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ ) by YELLOW_1:3; :: thesis: verum

end;

suppose A4: ( x <= sup I & not y <= sup I ) ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ )

then A5: (DownMap I) . x = (downarrow x) /\ I by Def16;
A6: (DownMap I) . y = downarrow y by A4, Def16;
A7: downarrow x c= downarrow y by A1, WAYBEL_0:21;
(downarrow x) /\ I c= downarrow x by XBOOLE_1:17;
then (DownMap I) . x c= (DownMap I) . y by A5, A6, A7;
hence for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ ) by YELLOW_1:3; :: thesis: verum

end;

suppose ( not x <= sup I & y <= sup I ) ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ )

hence for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ ) by A1, ORDERS_2:3; :: thesis: verum

end;

suppose A8: ( not x <= sup I & not y <= sup I ) ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ )

then A9: (DownMap I) . x = downarrow x by Def16;
(DownMap I) . y = downarrow y by A8, Def16;
then (DownMap I) . x c= (DownMap I) . y by A1, A9, WAYBEL_0:21;
hence for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (DownMap I) . x or not b₂ = (DownMap I) . y or b₁ <= b₂ ) by YELLOW_1:3; :: thesis: verum

end;

end;