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 ( r in REAL+ & s in REAL+ ) ; :: thesis: r = s

then ( ex r', s' being Element of REAL+ st
( r = r' & s = s' & r' <=' s' ) & ex s'', r'' being Element of REAL+ st
( s = s'' & r = r'' & s'' <=' r'' ) ) by A1, A2, XXREAL_0:def 5;
hence r = s by ARYTM_1:4; :: thesis: verum

end;

suppose A4: ( r in REAL+ & s in [:{0 },REAL+ :] ) ; :: thesis: r = s

then ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0 },REAL+ :] or not s in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence r = s by A1, A4, XXREAL_0:def 5; :: thesis: verum

end;

suppose A5: ( s in REAL+ & r in [:{0 },REAL+ :] ) ; :: thesis: r = s

then ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0 },REAL+ :] or not s in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence r = s by A2, A5, XXREAL_0:def 5; :: thesis: verum

end;

suppose A6: ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] ) ; :: thesis: r = s

consider r', s' being Element of REAL+ such that
A7: ( r = [0 ,r'] & s = [0 ,s'] ) and
A8: s' <=' r' by A1, A6, XXREAL_0:def 5;
consider s'', r'' being Element of REAL+ such that
A9: ( s = [0 ,s''] & r = [0 ,r''] ) and
A10: r'' <=' s'' by A2, A6, XXREAL_0:def 5;
( r' = r'' & s' = s'' ) by A7, A9, ZFMISC_1:33;
hence r = s by A8, A9, A10, ARYTM_1:4; :: thesis: verum

end;

end;