theorem Th26: :: ANPROJ_8:31

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