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 & (AR -below ) . y = AR -below y ) by Def13;
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, YELLOW_1:3; :: thesis: verum