let p1, p2 be Point of (TOP-REAL 3); (- 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; verum