let p be Point of (TOP-REAL 2); :: thesis: - p = |[(- (p `1)),(- (p `2))]|
thus - p = (- 1) * p
.= |[((- 1) * (p `1)),((- 1) * (p `2))]| by Th29
.= |[(- (p `1)),(- (p `2))]| ; :: thesis: verum