let x, y be ext-real number ; :: 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 XXREAL_3:def 1

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

y in REAL by A2, Lm2;
then consider b being complex number such that
A4: y = b and
A5: - y = - b by Def5;
x in REAL by A3, Lm2;
then consider a being complex number such that
A6: x = a and
A7: - x = - a by Def5;
( x in REAL & y in REAL ) by A2, A3, Lm2;
then reconsider a = a, b = b as real number by A4, A6;
reconsider mb = - b, ma = - a as Element of REAL by XREAL_0:def 1;
take mb ; :: thesis: ex q being Element of REAL st
( mb = - y & q = - x & mb <= q )
take ma ; :: thesis: ( mb = - y & ma = - x & mb <= ma )
thus ( mb = - y & ma = - x ) by A5, A7; :: thesis: mb <= ma
thus mb <= ma 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, Def1;
hence ( - y = -infty or - x = +infty ) by Def5; :: thesis: verum

end;

end;