theorem Th71: :: JORDAN2C:87

for n being Nat
for r being Real
for q being Point of (TOP-REAL n) st q = <*r*> holds
|.q.| = |.r.|