theorem Th74: :: EUCLID_8:83

for p1, p2 being Element of REAL 3 holds p1 <X> p2 = - (p2 <X> p1)