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