let g be Function of I[01],R^1; 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; ( 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]
; 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 )
; verum