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