let X be ComplexNormSpace; :: thesis: for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
let x, y be Point of X; :: thesis: ( ( for e being Real st e > 0 holds
||.(x - y).|| < e ) implies x = y )
assume for e being Real st e > 0 holds
||.(x - y).|| < e ; :: thesis: x = y
then x - y = 0. X by Lm1;
hence x = y by RLVECT_1:21; :: thesis: verum