:: deftheorem defines <X> EUCLID_5:def 4 :
for p1, p2 being Point of (TOP-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)))]|;