theorem :: NCFCONT2:39

for X being ComplexNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||