theorem Th31: :: EUCLID:59

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