theorem Th12: :: EUCLID13:13

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