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 )
now assume A3:
for
rc being
Element of
REAL holds
( not
f . rc = d or not
ra < rc or not
rc < rb )
;
:: thesis: contradictionA5:
the
carrier of
(Closed-Interval-TSpace ra,rb) = [.ra,rb.]
by A1, TOPMETR:25;
reconsider C =
f .: ([#] (Closed-Interval-TSpace ra,rb)) as
Subset of
R^1 ;
A6:
now assume
d in f .: ([#] (Closed-Interval-TSpace ra,rb))
;
:: thesis: contradictionthen consider x being
set such that A7:
(
x in the
carrier of
(Closed-Interval-TSpace ra,rb) &
x in [#] (Closed-Interval-TSpace ra,rb) &
d = f . x )
by FUNCT_2:115;
reconsider r =
x as
Real by A5, A7;
A8:
(
ra <= r &
r <= rb )
by A5, A7, XXREAL_1:1;
then A9:
ra < r
by A2, A7, XXREAL_0:1;
r < rb
by A2, A7, A8, XXREAL_0:1;
hence
contradiction
by A3, A7, A9;
:: thesis: verum end;
ra in [.ra,rb.]
by A1, XXREAL_1:1;
then A10:
ra in [#] (Closed-Interval-TSpace ra,rb)
by A5;
A11:
dom f = the
carrier of
(Closed-Interval-TSpace ra,rb)
by FUNCT_2:def 1;
then A12:
a in f .: ([#] (Closed-Interval-TSpace ra,rb))
by A2, A10, FUNCT_1:def 12;
rb in [#] (Closed-Interval-TSpace ra,rb)
by A1, A5, XXREAL_1:1;
then
b in f .: ([#] (Closed-Interval-TSpace ra,rb))
by A2, A11, FUNCT_1:def 12;
then
not
C is
connected
by A2, A6, A12, 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