theorem Th10: :: EUCLID_5:10

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