let ra, rb be real number ; :: thesis: for g being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
let g be continuous Function of (Closed-Interval-TSpace ra,rb),R^1 ; :: thesis: for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
let s1, s2 be real number ; :: thesis: ( ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb implies ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) )
assume that
A1: ra < rb and
A2: s1 * s2 < 0 ; :: thesis: ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) )
( ( s1 > 0 & s2 < 0 ) or ( s1 < 0 & s2 > 0 ) ) by A2, XREAL_1:135;
hence ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) ) by A1, Th12, Th13; :: thesis: verum