theorem Th2: :: TOPREAL9:4

for r being Real
for V being RealLinearSpace
for y, z being Point of V
for x being object st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )