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

|.(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