let r, s be Real; :: 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 r9, s9 being Element of REAL+ st
( r = r9 & s = s9 & r9 <=' s9 ) & ex s99, r99 being Element of REAL+ st
( s = s99 & r = r99 & s99 <=' r99 ) ) 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 r9, s9 being Element of REAL+ such that
A7: ( r = [0,r9] & s = [0,s9] ) and
A8: s9 <=' r9 by A1, A6, XXREAL_0:def 5;
consider s99, r99 being Element of REAL+ such that
A9: ( s = [0,s99] & r = [0,r99] ) and
A10: r99 <=' s99 by A2, A6, XXREAL_0:def 5;
( r9 = r99 & s9 = s99 ) by A7, A9, XTUPLE_0:1;
hence r = s by A8, A9, A10, ARYTM_1:4; :: thesis: verum

end;

end;