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 Th61
.= |[(- (p `1 )),(- (p `2 ))]| ; :: thesis: verum