theorem Th27: :: EUCLID_5:27

for p being Point of (TOP-REAL 3) holds p = <*(p `1),(p `2),(p `3)*>