theorem Th9: :: TOPREAL5:9

for g being Function of I[01],R^1
for s1, s2 being Real st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )