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;

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;

end;

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;( 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

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;hence r = s by A1, A4, XXREAL_0:def 5; :: thesis: verum

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;hence r = s by A2, A5, XXREAL_0:def 5; :: thesis: verum

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;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