theorem :: NORMSP_1:11

for RNS being RealNormSpace
for x, y being Point of RNS st x <> y holds
||.(x - y).|| <> 0 by Th6;