theorem Th25: :: TOPREAL6:27

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