let ra, rb be Real; :: thesis: for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for s1, s2 being Real st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being 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 st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Real st
( g . r1 = 0 & ra < r1 & r1 < rb )
let s1, s2 be Real; :: thesis: ( ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb implies ex r1 being 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 Real st
( g . r1 = 0 & ra < r1 & r1 < rb ) )
( ( s1 > 0 & s2 < 0 ) or ( s1 < 0 & s2 > 0 ) ) by A2, XREAL_1:133;
hence ( not s1 = g . ra or not s2 = g . rb or ex r1 being Real st
( g . r1 = 0 & ra < r1 & r1 < rb ) ) by A1, Th6, Th7; :: thesis: verum