let x, y be Element of L; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (R -LowerMap) . x <= (R -LowerMap) . y )

set s = R -LowerMap ;

A1: (R -LowerMap) . y = R -below y by Def2;

assume x <= y ; :: thesis: (R -LowerMap) . x <= (R -LowerMap) . y

then A2: R -below x c= R -below y by WAYBEL_4:17;

(R -LowerMap) . x = R -below x by Def2;

hence (R -LowerMap) . x <= (R -LowerMap) . y by A2, A1, YELLOW_1:3; :: thesis: verum

set s = R -LowerMap ;

A1: (R -LowerMap) . y = R -below y by Def2;

assume x <= y ; :: thesis: (R -LowerMap) . x <= (R -LowerMap) . y

then A2: R -below x c= R -below y by WAYBEL_4:17;

(R -LowerMap) . x = R -below x by Def2;

hence (R -LowerMap) . x <= (R -LowerMap) . y by A2, A1, YELLOW_1:3; :: thesis: verum