let r1, r2 be Real; :: thesis: ( ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ) implies r1 = r2 )
assume that
A2: for e1 being Real st e1 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e1 ) ) and
A3: for e2 being Real st e2 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e2 ) ) ; :: thesis: r1 = r2

A4: now

let e3 be real number ; :: thesis: ( e3 > 0 implies abs (r1 - r2) < e3 )
assume A5: e3 > 0 ; :: thesis: abs (r1 - r2) < e3
set e4 = e3 / 2;
A6: ( e3 / 2 is Real & e3 / 2 > 0 ) by A5, XREAL_1:141;
A7: (e3 / 2) + (e3 / 2) = e3 ;
consider Y01 being finite Subset of X such that
A8: ( not Y01 is empty & Y01 c= Y & ( for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e3 / 2 ) ) by A2, A6;
consider Y02 being finite Subset of X such that
A9: ( not Y02 is empty & Y02 c= Y & ( for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e3 / 2 ) ) by A3, A6;
set Y00 = Y01 \/ Y02;
A10: Y01 \/ Y02 c= Y by A8, A9, XBOOLE_1:8;
A11: ( Y01 \/ Y02 is finite Subset of X & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;
A12: abs (r2 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal )) < e3 / 2 by A9, A10, XBOOLE_1:7;
A13: abs ((r1 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal )) - (r2 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal ))) <= (abs (r1 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal ))) + (abs (r2 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal ))) by COMPLEX1:143;
(abs (r1 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal ))) + (abs (r2 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal ))) < e3 by A7, A8, A10, A11, A12, XREAL_1:10;
hence abs (r1 - r2) < e3 by A13, XXREAL_0:2; :: thesis: verum

end;

r1 = r2

proof

assume A14: r1 <> r2 ; :: thesis: contradiction
A15: abs (r1 - r2) <> 0

proof

assume abs (r1 - r2) = 0 ; :: thesis: contradiction
then r1 - r2 = 0 by ABSVALUE:7;
hence contradiction by A14; :: thesis: verum

end;

0 <= abs (r1 - r2) by COMPLEX1:132;
hence contradiction by A4, A15; :: thesis: verum

end;

hence r1 = r2 ; :: thesis: verum