let p1, p2 be Real; ( ( for e being Real st 0 < e holds
|.(p1 - p2).| < e ) implies p1 = p2 )
assume A1:
for e being Real st 0 < e holds
|.(p1 - p2).| < e
; p1 = p2
assume
p1 <> p2
; contradiction
then
p1 - p2 <> 0
;
then
0 < |.(p1 - p2).|
by COMPLEX1:47;
hence
contradiction
by A1; verum