let ra, rb, a, b be real number ; :: thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume A1: ra < rb ; :: thesis: for f being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
let f be continuous Function of (Closed-Interval-TSpace ra,rb),R^1 ; :: thesis: for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
let d be real number ; :: thesis: ( f . ra = a & f . rb = b & a > d & d > b implies ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume A2: ( f . ra = a & f . rb = b & a > d & d > b ) ; :: thesis: ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
A3: [#] (Closed-Interval-TSpace ra,rb) is connected by A1, Th6;
A5: the carrier of (Closed-Interval-TSpace ra,rb) = [.ra,rb.] by A1, TOPMETR:25;
A6: dom f = the carrier of (Closed-Interval-TSpace ra,rb) by FUNCT_2:def 1;

now

assume A7: for rc being Element of REAL st ra < rc & rc < rb holds
f . rc <> d ; :: thesis: contradiction

A8: now

assume d in f .: ([#] (Closed-Interval-TSpace ra,rb)) ; :: thesis: contradiction
then consider x being set such that
A9: ( x in dom f & x in [#] (Closed-Interval-TSpace ra,rb) & d = f . x ) by FUNCT_1:def 12;
x in [.ra,rb.] by A5, A9;
then reconsider r = x as Real ;
A10: ( ra <= r & r <= rb ) by A5, A9, XXREAL_1:1;
then A11: ra < r by A2, A9, XXREAL_0:1;
rb > r by A2, A9, A10, XXREAL_0:1;
hence contradiction by A7, A9, A11; :: thesis: verum

end;

ra in [.ra,rb.] by A1, XXREAL_1:1;
then A12: a in f .: ([#] (Closed-Interval-TSpace ra,rb)) by A2, A5, A6, FUNCT_1:def 12;
rb in [.ra,rb.] by A1, XXREAL_1:1;
then b in f .: ([#] (Closed-Interval-TSpace ra,rb)) by A2, A5, A6, FUNCT_1:def 12;
hence contradiction by A2, A3, A8, A12, Th9, TOPS_2:75; :: thesis: verum

end;

hence ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) ; :: thesis: verum