theorem :: EUCLID13:20

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 = 0 holds
Cn = Bn