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 )
then A2: the carrier of (Closed-Interval-TSpace (ra,rb)) = [.ra,rb.] by TOPMETR:18;
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
A3: f . ra = a and
A4: f . rb = b and
A5: a > d and
A6: d > b ; :: thesis: ex rc being Real st
( f . rc = d & ra < rc & rc < rb )
A7: dom f = the carrier of (Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def 1;
A8: [#] (Closed-Interval-TSpace (ra,rb)) is connected by A1, Th2;
now :: thesis: ex rc being Real st
( ra < rc & rc < rb & not f . rc <> d )
assume A9: for rc being Real st ra < rc & rc < rb holds
f . rc <> d ; :: 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 dom f and
x in [#] (Closed-Interval-TSpace (ra,rb)) and
A12: d = f . x by FUNCT_1:def 6;
x in [.ra,rb.] by A2, A11;
then reconsider r = x as Real ;
r <= rb by A2, A11, XXREAL_1:1;
then A13: rb > r by A4, A6, A12, XXREAL_0:1;
ra <= r by A2, A11, XXREAL_1:1;
then ra < r by A3, A5, A12, XXREAL_0:1;
hence contradiction by A9, A12, A13; :: thesis: verum
end;
rb in [.ra,rb.] by A1, XXREAL_1:1;
then A14: b in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A4, A2, A7, FUNCT_1:def 6;
ra in [.ra,rb.] by A1, XXREAL_1:1;
then a in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A3, A2, A7, FUNCT_1:def 6;
hence contradiction by A5, A6, A8, A10, A14, Th3, TOPS_2:61; :: thesis: verum
end;
hence ex rc being Real st
( f . rc = d & ra < rc & rc < rb ) ; :: thesis: verum