let X be non empty TopSpace; :: thesis: for xa, xb being Point of X
for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let xa, xb be Point of X; :: thesis: for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let a, b, d be Real; :: thesis: for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let f be continuous Function of X,R^1 ; :: thesis: ( X is connected & f . xa = a & f . xb = b & a <= d & d <= b implies ex xc being Point of X st f . xc = d )
assume A1: ( X is connected & f . xa = a & f . xb = b & a <= d & d <= b ) ; :: thesis: ex xc being Point of X st f . xc = d

now

assume A2: ( not a = d & not d = b ) ; :: thesis: ex xc being Point of X st f . xc = d
then A3: a < d by A1, XXREAL_0:1;
A4: d < b by A1, A2, XXREAL_0:1;

now

assume A5: for rc being Point of X holds not f . rc = d ; :: thesis: contradiction

A7: now

assume d in f .: ([#] X) ; :: thesis: contradiction
then consider x being set such that
A8: ( x in the carrier of X & x in [#] X & d = f . x ) by FUNCT_2:115;
thus contradiction by A5, A8; :: thesis: verum

end;

A10: dom f = the carrier of X by FUNCT_2:def 1;
then A11: a in f .: ([#] X) by A1, FUNCT_1:def 12;
A12: b in f .: ([#] X) by A1, A10, FUNCT_1:def 12;
[#] X is connected by A1, CONNSP_1:28;
hence contradiction by A3, A4, A7, A11, A12, Th9, TOPS_2:75; :: thesis: verum

end;

hence ex xc being Point of X st f . xc = d ; :: thesis: verum

end;

hence ex xc being Point of X st f . xc = d by A1; :: thesis: verum