let GX be non empty TopSpace; :: thesis: for A being Subset of GX st ( for xa, ya being Point of GX st xa in A & ya in A & xa <> ya holds
ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 ) ) holds
A is connected
let A be Subset of GX; :: thesis: ( ( for xa, ya being Point of GX st xa in A & ya in A & xa <> ya holds
ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 ) ) implies A is connected )
assume A1: for xa, ya being Point of GX st xa in A & ya in A & xa <> ya holds
ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 ) ; :: thesis: A is connected

per cases ( not A is empty or A is empty ) ;

suppose not A is empty ; :: thesis: A is connected

then reconsider A = A as non empty Subset of GX ;
A2: for xa, ya being Point of GX st xa in A & ya in A & xa = ya holds
ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 )

proof

let xa, ya be Point of GX; :: thesis: ( xa in A & ya in A & xa = ya implies ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 ) )
assume A3: ( xa in A & ya in A & xa = ya ) ; :: thesis: ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 )
then reconsider xa' = xa as Element of (GX | A) by PRE_TOPC:29;
reconsider h = I[01] --> xa' as Function of I[01] ,(GX | A) ;
take h ; :: thesis: ( h is continuous & xa = h . 0 & ya = h . 1 )
h = the carrier of I[01] --> xa' ;
hence ( h is continuous & xa = h . 0 & ya = h . 1 ) by A3, Lm1, BORSUK_1:83, FUNCOP_1:13; :: thesis: verum

end;

for xb, yb being Point of (GX | A) ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 )

proof

let xb, yb be Point of (GX | A); :: thesis: ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 )
( xb in [#] (GX | A) & yb in [#] (GX | A) ) ;
then A4: ( xb in A & yb in A ) by PRE_TOPC:def 10;

per cases ( xb <> yb or xb = yb ) ;

suppose xb <> yb ; :: thesis: ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 )

hence ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 ) by A1, A4; :: thesis: verum

end;

suppose xb = yb ; :: thesis: ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 )

hence ex ha being Function of I[01] ,(GX | A) st
( ha is continuous & xb = ha . 0 & yb = ha . 1 ) by A2, A4; :: thesis: verum

end;

end;

end;

then GX | A is connected by Th4;
hence A is connected by CONNSP_1:def 3; :: thesis: verum

end;

suppose A is empty ; :: thesis: A is connected

then reconsider D = A as empty Subset of GX ;
let A1, B1 be Subset of (GX | A); :: according to CONNSP_1:def 2,CONNSP_1:def 3 :: thesis: ( not [#] (GX | A) = A1 \/ B1 or not A1,B1 are_separated or A1 = {} (GX | A) or B1 = {} (GX | A) )
assume that
[#] (GX | A) = A1 \/ B1 and
A1,B1 are_separated ; :: thesis: ( A1 = {} (GX | A) or B1 = {} (GX | A) )
[#] (GX | D) = D by PRE_TOPC:def 10;
hence ( A1 = {} (GX | A) or B1 = {} (GX | A) ) ; :: thesis: verum

end;

end;