theorem :: CLVECT_1:112

for CNS being ComplexNormSpace
for x, y being Point of CNS st x <> y holds
||.(x - y).|| <> 0 by Th107;