theorem :: EUCLID_5:26

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