theorem :: EUCLID13:19

for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Cn = (r * An) + ((1 - r) * Bn) & r = 1 holds
Cn = An