let p1, p2 be Point of (TOP-REAL 3); :: thesis: p1 <X> p2 = - (p2 <X> p1)
- (p2 <X> p1) = (- 1) * (p2 <X> p1) by RLVECT_1:16
.= |[((- 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