theorem Th36: :: EUCLID_2:38

for n being Nat
for p being Point of (TOP-REAL n) holds 0 <= |.p.|