let ra, rb, a, b be Real; :: thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being Real st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being 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 st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being 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 st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Real st
( f . rc = d & ra < rc & rc < rb )
let d be Real; :: thesis: ( f . ra = a & f . rb = b & a < d & d < b implies ex rc being 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 Real st
( f . rc = d & ra < rc & rc < rb )

now :: thesis: ex rc being Real st
( f . rc = d & ra < rc & rc < rb )

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:18;
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 6;
assume A9: for rc being Real holds
( not f . rc = d or not ra < rc or not rc < rb ) ; :: thesis: contradiction

A10: now :: thesis: not d in f .: ([#] (Closed-Interval-TSpace (ra,rb)))

assume d in f .: ([#] (Closed-Interval-TSpace (ra,rb))) ; :: thesis: contradiction
then consider x being object 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:64;
reconsider r = x as Real by 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 6;
then not C is connected by A4, A5, A10, A8, Th3;
hence contradiction by A1, Th2, TOPS_2:61; :: thesis: verum

end;

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