let A be Point of (TOP-REAL 2); :: thesis: ( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) )
- A = |[(- (A `1)),(- (A `2))]| by EUCLID:59;
hence ( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) ) by EUCLID:52; :: thesis: verum