let a, b be Real; :: thesis: ( ( for c being Real st 0 < c holds
|.(a - b).| <= c ) implies a = b )
assume A1: for c being Real st 0 < c holds
|.(a - b).| <= c ; :: thesis: a = b
assume a <> b ; :: thesis: contradiction
then A2: a - b <> 0 ;
set e = |.(a - b).| / 2;
2 * (|.(a - b).| / 2) <= |.(a - b).| / 2 by A1;
then (2 * (|.(a - b).| / 2)) / (|.(a - b).| / 2) <= (|.(a - b).| / 2) / (|.(a - b).| / 2) by XREAL_1:72;
then 2 <= (|.(a - b).| / 2) / (|.(a - b).| / 2) by A2, XCMPLX_1:89;
then 2 <= 1 by A2, XCMPLX_1:60;
hence contradiction ; :: thesis: verum