for a being Real
for p, q, r being Point of (TOP-REAL 3) holds |{p,(a * q),r}| = a * |{p,q,r}|