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 that
A2: f . ra = a and
A3: f . rb = b and
A4: a < d and
A5: d < b ; :: thesis: ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )

now

reconsider C = f .: ([#] (Closed-Interval-TSpace ra,rb)) as Subset of R^1 ;
A6: dom f = the carrier of (Closed-Interval-TSpace ra,rb) by FUNCT_2:def 1;
A7: the carrier of (Closed-Interval-TSpace ra,rb) = [.ra,rb.] by A1, TOPMETR:25;
then rb in [#] (Closed-Interval-TSpace ra,rb) by A1, XXREAL_1:1;
then A8: b in f .: ([#] (Closed-Interval-TSpace ra,rb)) by A3, A6, FUNCT_1:def 12;
assume A9: for rc being Element of REAL holds
( not f . rc = d or not ra < rc or not rc < rb ) ; :: thesis: contradiction

A10: now

assume d in f .: ([#] (Closed-Interval-TSpace ra,rb)) ; :: thesis: contradiction
then consider x being set such that
A11: x in the carrier of (Closed-Interval-TSpace ra,rb) and
x in [#] (Closed-Interval-TSpace ra,rb) and
A12: d = f . x by FUNCT_2:115;
reconsider r = x as Real by A7, A11;
r <= rb by A7, A11, XXREAL_1:1;
then A13: r < rb by A3, A5, A12, XXREAL_0:1;
ra <= r by A7, A11, XXREAL_1:1;
then ra < r by A2, A4, A12, XXREAL_0:1;
hence contradiction by A9, A12, A13; :: thesis: verum

end;

ra in [#] (Closed-Interval-TSpace ra,rb) by A1, A7, XXREAL_1:1;
then a in f .: ([#] (Closed-Interval-TSpace ra,rb)) by A2, A6, FUNCT_1:def 12;
then not C is connected by A4, A5, A10, A8, Th9;
hence contradiction by A1, Th6, TOPS_2:75; :: thesis: verum

end;

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