let r, s be real number ; :: thesis: ( r <= s & s <= r implies r = s )
assume that
A1:
r <= s
and
A2:
s <= r
; :: thesis: r = s
A3:
( r in REAL & s in REAL )
by Def1;
per cases
( ( r in REAL+ & s in REAL+ ) or ( r in REAL+ & s in [:{0 },REAL+ :] ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] ) )
by A3, NUMBERS:def 1, XBOOLE_0:def 3;
suppose that A4:
r in REAL+
and A5:
s in REAL+
;
:: thesis: r = sconsider r',
s' being
Element of
REAL+ such that A6:
r = r'
and A7:
s = s'
and A8:
r' <=' s'
by A1, A4, A5, XXREAL_0:def 5;
consider s'',
r'' being
Element of
REAL+ such that A9:
s = s''
and A10:
r = r''
and A11:
s'' <=' r''
by A2, A4, A5, XXREAL_0:def 5;
thus
r = s
by A6, A7, A8, A9, A10, A11, ARYTM_1:4;
:: thesis: verum end; suppose that A14:
r in [:{0 },REAL+ :]
and A15:
s in [:{0 },REAL+ :]
;
:: thesis: r = sconsider r',
s' being
Element of
REAL+ such that A16:
r = [0 ,r']
and A17:
s = [0 ,s']
and A18:
s' <=' r'
by A1, A14, A15, XXREAL_0:def 5;
consider s'',
r'' being
Element of
REAL+ such that A19:
s = [0 ,s'']
and A20:
r = [0 ,r'']
and A21:
r'' <=' s''
by A2, A14, A15, XXREAL_0:def 5;
(
r' = r'' &
s' = s'' )
by A16, A17, A19, A20, ZFMISC_1:33;
hence
r = s
by A18, A19, A20, A21, ARYTM_1:4;
:: thesis: verum end;