theorem :: EUCLID_5:16

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