theorem Th3: :: SPRECT_3:3

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