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

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

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

now :: thesis: ex rc being Point of X st
( rc in B & f . rc = d )

assume A6: for rc being Point of X holds
( not rc in B or not f . rc = d ) ; :: thesis: contradiction

A7: now :: thesis: not d in f .: B

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

end;

dom f = the carrier of X by FUNCT_2:def 1;
then ( a in f .: B & b in f .: B ) by A2, A4, FUNCT_1:def 6;
hence contradiction by A1, A5, A7, Th3, TOPS_2:61; :: thesis: verum

end;

hence ex xc being Point of X st
( xc in B & f . xc = d ) ; :: thesis: verum

end;

hence ex xc being Point of X st
( xc in B & f . xc = d ) by A2, A4; :: thesis: verum