theorem Th24: :: EUCLID_5:24

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