let p1, p2 be Element of REAL 3; :: thesis: p1 <X> p2 = - (p2 <X> p1)
- (p2 <X> p1) = |[((- 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 Th50
.= p1 <X> p2 ;
hence p1 <X> p2 = - (p2 <X> p1) ; :: thesis: verum