theorem Th1: :: BROUWER2:1

for n being Nat
for p, q being Point of (TOP-REAL n)
for r being Real holds ((1 - r) * p) + (r * q) = p + (r * (q - p))