for a, b being Real st ( for c being Real st 0 < c holds
|.(a - b).| <= c ) holds
a = b