let g be Function of I[01],R^1; :: thesis: for s1, s2, r being Real 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; :: 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 14, BORSUK_1:def 15, TOPMETR:20, TOPREAL5:6;
hence ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) ; :: thesis: verum