theorem Th6: :: NORMSP_1:6

for RNS being RealNormSpace
for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )