let T be non empty TopSpace; :: thesis: for f being continuous RealMap of T
for A being Subset of T st A is connected holds
f .: A is interval

let f be continuous RealMap of T; :: thesis: for A being Subset of T st A is connected holds
f .: A is interval

let A be Subset of T; :: thesis: ( A is connected implies f .: A is interval )
assume A1: A is connected ; :: thesis: f .: A is interval
let r, s be ExtReal; :: according to XXREAL_2:def 12 :: thesis: ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A )
A2: A c= f " (f .: A) by FUNCT_2:42;
assume A3: r in f .: A ; :: thesis: ( not s in f .: A or [.r,s.] c= f .: A )
then consider p being Point of T such that
A4: p in A and
A5: r = f . p by FUNCT_2:65;
assume A6: s in f .: A ; :: thesis: [.r,s.] c= f .: A
then consider q being Point of T such that
A7: q in A and
A8: s = f . q by FUNCT_2:65;
assume A9: not [.r,s.] c= f .: A ; :: thesis: contradiction
reconsider r = r, s = s as Real by A3, A6;
consider t being Element of REAL such that
A10: t in [.r,s.] and
A11: not t in f .: A by A9;
reconsider r = r, s = s, t = t as Real ;
set P1 = f " ;
set Q1 = f " ;
set P = (f " ) /\ A;
set Q = (f " ) /\ A;
set X = \/ ;
A12: f " is open by PSCOMP_1:8;
t <= s by ;
then A13: t < s by ;
right_open_halfline t = { r1 where r1 is Real : t < r1 } by XXREAL_1:230;
then s in right_open_halfline t by A13;
then q in f " by ;
then A14: (f " ) /\ A <> {} T by ;
/\ = ].t,t.[ by XXREAL_1:269
.= {} by XXREAL_1:28 ;
then left_open_halfline t misses right_open_halfline t ;
then f " misses f " by FUNCT_1:71;
then (f " ) /\ (f " ) = {} ;
then A15: (f " ) /\ (f " ) misses ((f " ) /\ A) \/ ((f " ) /\ A) ;
reconsider Y = {t} as Subset of REAL ;
Y ` = REAL \ [.t,t.] by XXREAL_1:17
.= \/ by XXREAL_1:385 ;
then A16: (f " Y) ` = f " () by FUNCT_2:100
.= (f " ) \/ (f " ) by RELAT_1:140 ;
f " {t} misses f " (f .: A) by ;
then f " {t} misses A by ;
then A c= (f " ) \/ (f " ) by ;
then A17: A = A /\ ((f " ) \/ (f " )) by XBOOLE_1:28
.= ((f " ) /\ A) \/ ((f " ) /\ A) by XBOOLE_1:23 ;
A18: (f " ) /\ A c= f " by XBOOLE_1:17;
r <= t by ;
then A19: r < t by ;
left_open_halfline t = { r1 where r1 is Real : r1 < t } by XXREAL_1:229;
then r in left_open_halfline t by A19;
then p in f " by ;
then A20: (f " ) /\ A <> {} T by ;
A21: (f " ) /\ A c= f " by XBOOLE_1:17;
f " is open by PSCOMP_1:8;
then (f " ) /\ A,(f " ) /\ A are_separated by ;
hence contradiction by A1, A17, A20, A14, CONNSP_1:15; :: thesis: verum