let X be non empty TopSpace; :: thesis:
let xa, xb be Point of X; :: thesis:
let B be Subset of X; :: thesis:
let a, b, d be Real; :: thesis:
let f be continuous Function of X,R^1 ; :: thesis:
assume A1: ( B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B ) ; :: thesis:

now

assume A2: ( not a = d & not d = b ) ; :: thesis:
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 rc in B or not f . rc = d ) ; :: thesis:

A6: now

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

end;

A8: dom f = the carrier of X by FUNCT_2:def 1;
then A9: a in f .: B by A1, FUNCT_1:def 12;
b in f .: B by A1, A8, FUNCT_1:def 12;
hence contradiction by A1, A3, A4, A6, A9, Th9, TOPS_2:75; :: thesis:

end;

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

end;

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