let x, y be ExtReal; :: 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 )

x in REAL by A3, Lm3;
then consider a being Complex such that
A4: x = a and
A5: - x = - a by Def3;
y in REAL by A2, Lm3;
then consider b being Complex such that
A6: y = b and
A7: - y = - b by Def3;
( x in REAL & y in REAL ) by A2, A3, Lm3;
then reconsider a = a, b = b as Real by A6, A4;
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 A7, A5; :: thesis: mb <= ma
thus mb <= ma by A1, A6, A4, XREAL_1:24; :: 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 Lm3;
then ( x = -infty or y = +infty ) by A1, Def1;
hence ( - y = -infty or - x = +infty ) by Def3; :: thesis: verum

end;

end;