let p1, p2 be Real; :: thesis: ( ( 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 ; :: thesis: p1 = p2
assume p1 <> p2 ; :: thesis: contradiction
then p1 - p2 <> 0 ;
then 0 < |.(p1 - p2).| by COMPLEX1:47;
hence contradiction by A1; :: thesis: verum