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 ) or ( s in REAL+ & r in ) or ( r in & s in ) ) by ;
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 ;
hence r = s by ARYTM_1:4; :: thesis: verum
end;
suppose A4: ( r in REAL+ & s in ) ; :: thesis: r = s
then ( ( not r in REAL+ or not s in REAL+ ) & ( not r in or not s in ) ) by ;
hence r = s by ; :: thesis: verum
end;
suppose A5: ( s in REAL+ & r in ) ; :: thesis: r = s
then ( ( not r in REAL+ or not s in REAL+ ) & ( not r in or not s in ) ) by ;
hence r = s by ; :: thesis: verum
end;
suppose A6: ( r in & s in ) ; :: thesis: r = s
consider r9, s9 being Element of REAL+ such that
A7: ( r = [0,r9] & s = [0,s9] ) and
A8: s9 <=' r9 by ;
consider s99, r99 being Element of REAL+ such that
A9: ( s = [0,s99] & r = [0,r99] ) and
A10: r99 <=' s99 by ;
( r9 = r99 & s9 = s99 ) by ;
hence r = s by ; :: thesis: verum
end;
end;