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] 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] implies ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) )
assume that
A1: g is continuous and
A2: g . 0[01] < r and
A3: r < g . 1[01] ; :: thesis: ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
ex rc being Real st
( g . rc = r & 0 < rc & rc < 1 ) by A1, A2, A3, 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