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

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