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