let x, y be R_eal; :: thesis: ( x <= y implies - y <= - x )
assume A1: x <= y ; :: thesis: - y <= - x

per cases ( ( - y in REAL & - x in REAL ) or not - y in REAL or not - x in REAL ) ;
:: according to SUPINF_1:def 7

case that A2: - y in REAL and
A3: - x in REAL ; :: thesis: ex b₁, b₂ being Element of REAL st
( b₁ = - y & b₂ = - x & b₁ <= b₂ )

y in REAL by A2, Lm2;
then consider b being Real such that
A4: y = b and
A5: - y = - b by Def3;
x in REAL by A3, Lm2;
then consider a being Real such that
A6: x = a and
A7: - x = - a by Def3;
take - b ; :: thesis: ex b₁ being Element of REAL st
( - b = - y & b₁ = - x & - b <= b₁ )
take - a ; :: thesis: ( - b = - y & - a = - x & - b <= - a )
thus ( - b = - y & - a = - x ) by A5, A7; :: thesis: - b <= - a
thus - b <= - a by A1, A4, A6, XREAL_1:26; :: thesis: verum

end;

case ( not - y in REAL or not - x in REAL ) ; :: thesis: ( - y = -infty or - x = +infty )

then ( not y in REAL or not x in REAL ) by Lm2;
then ( x = -infty or y = +infty ) by A1, SUPINF_1:def 7;
hence ( - y = -infty or - x = +infty ) by Def3, Lm1; :: thesis: verum

end;

end;