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 that
A1: X is connected and
A2: ( f . xa = a & f . xb = b ) and
A3: ( a <= d & d <= b ) ; :: thesis: ex xc being Point of X st f . xc = d

now :: thesis: ( not a = d & not d = b implies ex xc being Point of X st f . xc = d )

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

now :: thesis: ex rc being Point of X st f . rc = d

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

A6: now :: thesis: not d in f .: ([#] X)

assume d in f .: ([#] X) ; :: thesis: contradiction
then ex x being object st
( x in the carrier of X & x in [#] X & d = f . x ) by FUNCT_2:64;
hence contradiction by A5; :: thesis: verum

end;

dom f = the carrier of X by FUNCT_2:def 1;
then A7: ( a in f .: ([#] X) & b in f .: ([#] X) ) by A2, FUNCT_1:def 6;
[#] X is connected by A1, CONNSP_1:27;
hence contradiction by A4, A6, A7, Th3, TOPS_2:61; :: 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 A2; :: thesis: verum