let x, y be ExtReal; ( x <= y implies - y <= - x )
assume A1:
x <= y
; - y <= - x
per cases
( ( - y in REAL & - x in REAL ) or not - y in REAL or not - x in REAL )
;
XXREAL_3:def 1case that A2:
- y in REAL
and A3:
- x in REAL
;
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
;
ex q being Element of REAL st
( mb = - y & q = - x & mb <= q )take
ma
;
( mb = - y & ma = - x & mb <= ma )thus
(
mb = - y &
ma = - x )
by A7, A5;
mb <= mathus
mb <= ma
by A1, A6, A4, XREAL_1:24;
verum end; end;