set s = R -LowerMap ;
let x, y be Element of L; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (R -LowerMap ) . x <= (R -LowerMap ) . y )
A1: ( (R -LowerMap ) . x = R -below x & (R -LowerMap ) . y = R -below y ) by Def2;
assume x <= y ; :: thesis: (R -LowerMap ) . x <= (R -LowerMap ) . y
then R -below x c= R -below y by WAYBEL_4:17;
hence (R -LowerMap ) . x <= (R -LowerMap ) . y by A1, YELLOW_1:3; :: thesis: verum