theorem :: EUCLID_5:18

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