theorem Th23: :: EUCLID_5:23

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