let L be non empty Poset; :: thesis: IdsMap L is monotone
let x1, x2 be Element of L; :: according to ORDERS_3:def 5 :: thesis: ( not x1 <= x2 or for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (IdsMap L) . x1 or not b₂ = (IdsMap L) . x2 or b₁ <= b₂ ) )
assume x1 <= x2 ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (IdsMap L) . x1 or not b₂ = (IdsMap L) . x2 or b₁ <= b₂ )
then downarrow x1 c= downarrow x2 by WAYBEL_0:21;
then (IdsMap L) . x1 c= downarrow x2 by Def4;
then A1: (IdsMap L) . x1 c= (IdsMap L) . x2 by Def4;
let a, b be Element of (InclPoset (Ids L)); :: thesis: ( not a = (IdsMap L) . x1 or not b = (IdsMap L) . x2 or a <= b )
assume ( a = (IdsMap L) . x1 & b = (IdsMap L) . x2 ) ; :: thesis: a <= b
hence a <= b by A1, YELLOW_1:3; :: thesis: verum