let p1, p2 be Point of (TOP-REAL 3); :: thesis: (- p1) <X> p2 = p1 <X> (- p2)
(- p1) <X> p2 = |[(- (p1 `1 )),(- (p1 `2 )),(- (p1 `3 ))]| <X> p2 by Th10
.= |[(- (p1 `1 )),(- (p1 `2 )),(- (p1 `3 ))]| <X> |[(p2 `1 ),(p2 `2 ),(p2 `3 )]| by Th3
.= |[(((- (p1 `2 )) * (p2 `3 )) - ((- (p1 `3 )) * (p2 `2 ))),(((- (p1 `3 )) * (p2 `1 )) - ((- (p1 `1 )) * (p2 `3 ))),(((- (p1 `1 )) * (p2 `2 )) - ((- (p1 `2 )) * (p2 `1 )))]| by Th15
.= |[(((p1 `2 ) * (- (p2 `3 ))) - ((p1 `3 ) * (- (p2 `2 )))),(((p1 `3 ) * (- (p2 `1 ))) - ((p1 `1 ) * (- (p2 `3 )))),(((p1 `1 ) * (- (p2 `2 ))) - ((p1 `2 ) * (- (p2 `1 ))))]|
.= |[(p1 `1 ),(p1 `2 ),(p1 `3 )]| <X> |[(- (p2 `1 )),(- (p2 `2 )),(- (p2 `3 ))]| by Th15
.= |[(p1 `1 ),(p1 `2 ),(p1 `3 )]| <X> (- p2) by Th10 ;
hence (- p1) <X> p2 = p1 <X> (- p2) by Th3; :: thesis: verum