theorem Th17: :: EUCLID_5:17

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