let g be Function of I[01] ,R^1 ; :: thesis: for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
let s1, s2, r be real number ; :: thesis: ( g is continuous & g . 0[01] < r & r < g . 1[01] & s1 = g . 0 & s2 = g . 1 implies ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) )
assume ( g is continuous & g . 0[01] < r & r < g . 1[01] & s1 = g . 0 & s2 = g . 1 ) ; :: thesis: ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
then ex rc being Real st
( g . rc = r & 0 < rc & rc < 1 ) by BORSUK_1:def 17, BORSUK_1:def 18, TOPMETR:27, TOPREAL5:12;
hence ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) ; :: thesis: verum