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 that
A3: xa in A and
ya in A and
A4: xa = ya ; :: thesis: ex h being Function of I[01],(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 )
reconsider xa9 = xa as Element of (GX | A) by A3, PRE_TOPC:8;
reconsider h = I[01] --> xa9 as Function of I[01],(GX | A) ;
take h ; :: thesis: ( h is continuous & xa = h . 0 & ya = h . 1 )
thus ( h is continuous & xa = h . 0 & ya = h . 1 ) by A4, Lm1, BORSUK_1:40, FUNCOP_1:7; :: 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 )
A5: xb in [#] (GX | A) ;
A6: yb in [#] (GX | A) ;
A7: xb in A by A5, PRE_TOPC:def 5;
A8: yb in A by A6, PRE_TOPC:def 5;
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, A7, A8; :: 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, A7; :: thesis: verum
end;
end;
end;
then GX | A is connected by Th1;
hence A is connected ; :: 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 ;
hence ( A1 = {} (GX | A) or B1 = {} (GX | A) ) ; :: thesis: verum
end;
end;