let a, b be ext-real number ; :: thesis: ( a <= b & b <= a implies a = b )
assume that
A1:
a <= b
and
A2:
b <= a
; :: thesis: a = b
per cases
( ( a in REAL+ & b in REAL+ ) or ( a in REAL+ & b in [:{0 },REAL+ :] ) or ( b in REAL+ & a in [:{0 },REAL+ :] ) or ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] ) or ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) or ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] ) & ( not b in REAL+ or not a in [:{0 },REAL+ :] ) & ( not a in REAL+ or not b in [:{0 },REAL+ :] ) ) )
;
suppose that A3:
a in REAL+
and A4:
b in REAL+
;
:: thesis: a = bconsider a',
b' being
Element of
REAL+ such that A5:
a = a'
and A6:
b = b'
and A7:
a' <=' b'
by A1, A3, A4, Def5;
consider b'',
a'' being
Element of
REAL+ such that A8:
b = b''
and A9:
a = a''
and A10:
b'' <=' a''
by A2, A3, A4, Def5;
thus
a = b
by A5, A6, A7, A8, A9, A10, ARYTM_1:4;
:: thesis: verum end; suppose that A13:
a in [:{0 },REAL+ :]
and A14:
b in [:{0 },REAL+ :]
;
:: thesis: a = bconsider a',
b' being
Element of
REAL+ such that A15:
a = [0 ,a']
and A16:
b = [0 ,b']
and A17:
b' <=' a'
by A1, A13, A14, Def5;
consider b'',
a'' being
Element of
REAL+ such that A18:
b = [0 ,b'']
and A19:
a = [0 ,a'']
and A20:
a'' <=' b''
by A2, A13, A14, Def5;
(
a' = a'' &
b' = b'' )
by A15, A16, A18, A19, ZFMISC_1:33;
hence
a = b
by A17, A18, A19, A20, ARYTM_1:4;
:: thesis: verum end;