set s = AR -below ;
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₁ = (AR -below) . x or not b₂ = (AR -below) . y or b₁ <= b₂ ) )
A1: (AR -below) . x = AR -below x by Def12;
A2: (AR -below) . y = AR -below y by Def12;
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (AR -below) . x or not b₂ = (AR -below) . y or b₁ <= b₂ )
then AR -below x c= AR -below y by Th17;
hence for b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) holds
( not b₁ = (AR -below) . x or not b₂ = (AR -below) . y or b₁ <= b₂ ) by A1, A2, YELLOW_1:3; :: thesis: verum