:: deftheorem defines <X> EUCLID_8:def 4 :
for p1, p2 being Element of REAL 3 holds p1 <X> p2 = |[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]|;