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