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