theorem Th4: :: SPRECT_3:4

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