theorem :: NCFCONT2:38

for X being ComplexNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )