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;
consider Y01 being finite Subset of X such that
not Y01 is empty and
A6: Y01 c= Y and
A7: 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, A5, XREAL_1:141;
consider Y02 being finite Subset of X such that
not Y02 is empty and
A8: Y02 c= Y and
A9: 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, A5, XREAL_1:141;
set Y00 = Y01 \/ Y02;
A10: ( (e3 / 2) + (e3 / 2) = e3 & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;
A11: Y01 \/ Y02 c= Y by A6, A8, XBOOLE_1:8;
then abs (r2 - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,L,addreal )) < e3 / 2 by A9, XBOOLE_1:7;
then ( 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 ))) & (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, A11, A10, COMPLEX1:143, XREAL_1:10;
hence abs (r1 - r2) < e3 by XXREAL_0:2; :: thesis: verum

end;

r1 = r2

proof

assume A12: r1 <> r2 ; :: thesis: contradiction
A13: abs (r1 - r2) <> 0

proof

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

end;

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

end;

hence r1 = r2 ; :: thesis: verum