theorem Th3: :: EUCLID_5:3

for p being Point of (TOP-REAL 3) holds p = |[(p `1),(p `2),(p `3)]|