:: CONNSP_1 semantic presentation

begin


definition
let GX be TopStruct ;
let A, B be Subset of GX;
predA,B are_separated  means :Def1: :: CONNSP_1:def 1
( Cl A misses B & A misses Cl B );
symmetry
 for A, B being Subset of GX st Cl A misses B & A misses Cl B holds
( Cl B misses A & B misses Cl A ) ;
end;

:: deftheorem Def1 defines are_separated CONNSP_1:def_1_:_
 for GX being TopStruct
for A, B being Subset of GX holds
( A,B are_separated iff ( Cl A misses B & A misses Cl B ) );

theorem Th1: :: CONNSP_1:1
for TS being TopStruct
for K, L being Subset of TS st K,L are_separated holds
K misses L
proof
let TS be TopStruct ; ::_thesis: for K, L being Subset of TS st K,L are_separated holds
K misses L
let K, L be Subset of TS; ::_thesis: ( K,L are_separated implies K misses L )
assume that
A1: (Cl K) /\ L = {} and
 K /\ (Cl L) = {} ; :: according to XBOOLE_0:def_7,CONNSP_1:def_1 ::_thesis: K misses L
 K c= Cl K by PRE_TOPC:18;
hence  K /\ L = {} by A1, XBOOLE_1:3, XBOOLE_1:27; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th2: :: CONNSP_1:2
for TS being TopStruct
for K, L being Subset of TS st K is closed & L is closed & K misses L holds
K,L are_separated
proof
let TS be TopStruct ; ::_thesis: for K, L being Subset of TS st K is closed & L is closed & K misses L holds
K,L are_separated
let K, L be Subset of TS; ::_thesis: ( K is closed & L is closed & K misses L implies K,L are_separated )
assume that
A1: K is closed and
A2: L is closed and
A3: K misses L ; ::_thesis: K,L are_separated
A4: K /\ L = {} by A3, XBOOLE_0:def_7;
 K /\ (Cl L) = K /\ L by A2, PRE_TOPC:22;
then A5: K misses Cl L by A4, XBOOLE_0:def_7;
 (Cl K) /\ L = K /\ L by A1, PRE_TOPC:22;
then  Cl K misses L by A4, XBOOLE_0:def_7;
hence  K,L are_separated by A5, Def1; ::_thesis: verum
end;

theorem Th3: :: CONNSP_1:3
for GX being TopSpace
for A, B being Subset of GX st [#] GX = A \/ B & A is open & B is open & A misses B holds
A,B are_separated
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX st [#] GX = A \/ B & A is open & B is open & A misses B holds
A,B are_separated
let A, B be Subset of GX; ::_thesis: ( [#] GX = A \/ B & A is open & B is open & A misses B implies A,B are_separated )
assume that
A1: [#] GX = A \/ B and
A2: A is open and
A3: B is open and
A4: A misses B ; ::_thesis: A,B are_separated
A5: Cl (([#] GX) \ B) = ([#] GX) \ B by A3, PRE_TOPC:23;
 A = ([#] GX) \ B by A1, A4, PRE_TOPC:5;
then A6: A is closed by A5, PRE_TOPC:22;
A7: Cl (([#] GX) \ A) = ([#] GX) \ A by A2, PRE_TOPC:23;
 B = ([#] GX) \ A by A1, A4, PRE_TOPC:5;
then  B is closed by A7, PRE_TOPC:22;
hence  A,B are_separated by A4, A6, Th2; ::_thesis: verum
end;

theorem Th4: :: CONNSP_1:4
for GX being TopSpace
for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated holds
( A is open & A is closed & B is open & B is closed )
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated holds
( A is open & A is closed & B is open & B is closed )
let A, B be Subset of GX; ::_thesis: ( [#] GX = A \/ B & A,B are_separated implies ( A is open & A is closed & B is open & B is closed ) )
assume that
A1: [#] GX = A \/ B and
A2: A,B are_separated ; ::_thesis: ( A is open & A is closed & B is open & B is closed )
A3: ([#] GX) \ B = A by A1, A2, Th1, PRE_TOPC:5;
A4: B c= Cl B by PRE_TOPC:18;
A5: now__::_thesis:_(_A_misses_Cl_B_implies_Cl_B_=_B_)
assume  A misses Cl B ; ::_thesis: Cl B = B
then  Cl B c= B by A1, XBOOLE_1:73;
hence  Cl B = B by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
A6: A c= Cl A by PRE_TOPC:18;
A7: now__::_thesis:_(_Cl_A_misses_B_implies_Cl_A_=_A_)
assume  Cl A misses B ; ::_thesis: Cl A = A
then  Cl A c= A by A1, XBOOLE_1:73;
hence  Cl A = A by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
 B = ([#] GX) \ A by A1, A2, Th1, PRE_TOPC:5;
hence  ( A is open & A is closed & B is open & B is closed ) by A2, A7, A5, A3, Def1, PRE_TOPC:22, PRE_TOPC:23; ::_thesis: verum
end;

theorem Th5: :: CONNSP_1:5
for GX being TopSpace
for X9 being SubSpace of GX
for P1, Q1 being Subset of GX
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
proof
let GX be TopSpace; ::_thesis: for X9 being SubSpace of GX
for P1, Q1 being Subset of GX
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let X9 be SubSpace of GX; ::_thesis: for P1, Q1 being Subset of GX
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let P1, Q1 be Subset of GX; ::_thesis: for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let P, Q be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated )
assume that
A1: P = P1 and
A2: Q = Q1 ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated )
reconsider P2 = P, Q2 = Q as Subset of GX by PRE_TOPC:11;
assume that
A3: (Cl P) /\ Q = {} and
A4: P /\ (Cl Q) = {} ; :: according to XBOOLE_0:def_7,CONNSP_1:def_1 ::_thesis: P1,Q1 are_separated
P /\ (Cl Q) = P /\ (([#] X9) /\ (Cl Q2)) by PRE_TOPC:17
.= (P /\ ([#] X9)) /\ (Cl Q2) by XBOOLE_1:16
.= P2 /\ (Cl Q2) by XBOOLE_1:28 ;
then A5: P2 misses Cl Q2 by A4, XBOOLE_0:def_7;
(Cl P) /\ Q = ((Cl P2) /\ ([#] X9)) /\ Q by PRE_TOPC:17
.= (Cl P2) /\ (Q /\ ([#] X9)) by XBOOLE_1:16
.= (Cl P2) /\ Q2 by XBOOLE_1:28 ;
then  Cl P2 misses Q2 by A3, XBOOLE_0:def_7;
hence  P1,Q1 are_separated by A1, A2, A5, Def1; ::_thesis: verum
end;

theorem Th6: :: CONNSP_1:6
for GX being TopSpace
for X9 being SubSpace of GX
for P, Q being Subset of GX
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
proof
let GX be TopSpace; ::_thesis: for X9 being SubSpace of GX
for P, Q being Subset of GX
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let X9 be SubSpace of GX; ::_thesis: for P, Q being Subset of GX
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let P, Q be Subset of GX; ::_thesis: for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let P1, Q1 be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated implies P1,Q1 are_separated )
assume that
A1: P = P1 and
A2: Q = Q1 and
A3: P \/ Q c= [#] X9 ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated )
A4: Q c= P \/ Q by XBOOLE_1:7;
 P c= P \/ Q by XBOOLE_1:7;
then reconsider P2 = P, Q2 = Q as Subset of X9 by A3, A4, XBOOLE_1:1;
assume that
A5: (Cl P) /\ Q = {} and
A6: P /\ (Cl Q) = {} ; :: according to XBOOLE_0:def_7,CONNSP_1:def_1 ::_thesis: P1,Q1 are_separated
P2 /\ (Cl Q2) = P2 /\ (([#] X9) /\ (Cl Q)) by PRE_TOPC:17
.= (P2 /\ ([#] X9)) /\ (Cl Q) by XBOOLE_1:16
.= P /\ (Cl Q) by XBOOLE_1:28 ;
then A7: P2 misses Cl Q2 by A6, XBOOLE_0:def_7;
 Cl P2 = (Cl P) /\ ([#] X9) by PRE_TOPC:17;
then (Cl P2) /\ Q2 = (Cl P) /\ (Q2 /\ ([#] X9)) by XBOOLE_1:16
.= (Cl P) /\ Q by XBOOLE_1:28 ;
then  Cl P2 misses Q2 by A5, XBOOLE_0:def_7;
hence  P1,Q1 are_separated by A1, A2, A7, Def1; ::_thesis: verum
end;

theorem Th7: :: CONNSP_1:7
for TS being TopStruct
for K, L, K1, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated
proof
let TS be TopStruct ; ::_thesis: for K, L, K1, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated
let K, L, K1, L1 be Subset of TS; ::_thesis: ( K,L are_separated & K1 c= K & L1 c= L implies K1,L1 are_separated )
assume that
A1: (Cl K) /\ L = {} and
A2: K /\ (Cl L) = {} and
A3: K1 c= K and
A4: L1 c= L ; :: according to XBOOLE_0:def_7,CONNSP_1:def_1 ::_thesis: K1,L1 are_separated
 Cl L1 c= Cl L by A4, PRE_TOPC:19;
then  K1 /\ (Cl L1) = {} TS by A2, A3, XBOOLE_1:3, XBOOLE_1:27;
then A5: K1 misses Cl L1 by XBOOLE_0:def_7;
 Cl K1 c= Cl K by A3, PRE_TOPC:19;
then  (Cl K1) /\ L1 = {} TS by A1, A4, XBOOLE_1:3, XBOOLE_1:27;
then  Cl K1 misses L1 by XBOOLE_0:def_7;
hence  K1,L1 are_separated by A5, Def1; ::_thesis: verum
end;

theorem Th8: :: CONNSP_1:8
for GX being TopSpace
for A, B, C being Subset of GX st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
proof
let GX be TopSpace; ::_thesis: for A, B, C being Subset of GX st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
let A, B, C be Subset of GX; ::_thesis: ( A,B are_separated & A,C are_separated implies A,B \/ C are_separated )
assume that
A1: Cl A misses B and
A2: A misses Cl B and
A3: Cl A misses C and
A4: A misses Cl C ; :: according to CONNSP_1:def_1 ::_thesis: A,B \/ C are_separated
A5: A /\ (Cl B) = {} by A2, XBOOLE_0:def_7;
A /\ (Cl (B \/ C)) = A /\ ((Cl B) \/ (Cl C)) by PRE_TOPC:20
.= (A /\ (Cl B)) \/ (A /\ (Cl C)) by XBOOLE_1:23
.= {} GX by A4, A5, XBOOLE_0:def_7 ;
then A6: A misses Cl (B \/ C) by XBOOLE_0:def_7;
A7: (Cl A) /\ B = {} by A1, XBOOLE_0:def_7;
(Cl A) /\ (B \/ C) = ((Cl A) /\ B) \/ ((Cl A) /\ C) by XBOOLE_1:23
.= {} GX by A3, A7, XBOOLE_0:def_7 ;
then  Cl A misses B \/ C by XBOOLE_0:def_7;
hence  A,B \/ C are_separated by A6, Def1; ::_thesis: verum
end;

theorem Th9: :: CONNSP_1:9
for TS being TopStruct
for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds
K \ L,L \ K are_separated
proof
let TS be TopStruct ; ::_thesis: for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds
K \ L,L \ K are_separated
let K, L be Subset of TS; ::_thesis: ( ( ( K is closed & L is closed ) or ( K is open & L is open ) ) implies K \ L,L \ K are_separated )
A1: now__::_thesis:_for_K,_L_being_Subset_of_TS_st_K_is_open_&_L_is_open_holds_
K_\_L,L_\_K_are_separated
let K, L be Subset of TS; ::_thesis: ( K is open & L is open implies K \ L,L \ K are_separated )
assume that
A2: K is open and
A3: L is open ; ::_thesis: K \ L,L \ K are_separated
A4: K /\ (L `) c= K by XBOOLE_1:17;
A5: (Cl L) /\ (K `) c= K ` by XBOOLE_1:17;
 Cl (([#] TS) \ K) = ([#] TS) \ K by A2, PRE_TOPC:23;
then A6: (K /\ (L `)) /\ ((Cl L) /\ (Cl (K `))) c= K /\ (K `) by A4, A5, XBOOLE_1:27;
A7: K \ L = K /\ (L `) by SUBSET_1:13;
A8: L /\ (K `) c= L by XBOOLE_1:17;
 (Cl K) /\ (L `) c= L ` by XBOOLE_1:17;
then A9: ((Cl K) /\ (L `)) /\ (L /\ (K `)) c= L /\ (L `) by A8, XBOOLE_1:27;
 L misses L ` by XBOOLE_1:79;
then A10: L /\ (L `) = {} by XBOOLE_0:def_7;
 K misses K ` by XBOOLE_1:79;
then A11: K /\ (K `) = {} by XBOOLE_0:def_7;
 ([#] TS) \ K = K ` ;
then A12: ((Cl K) /\ (Cl (L `))) /\ (L /\ (K `)) = ((Cl K) /\ (L `)) /\ (L /\ (K `)) by A3, PRE_TOPC:23;
A13: L \ K = L /\ (K `) by SUBSET_1:13;
 Cl (L /\ (K `)) c= (Cl L) /\ (Cl (K `)) by PRE_TOPC:21;
then  (K \ L) /\ (Cl (L \ K)) c= (K /\ (L `)) /\ ((Cl L) /\ (Cl (K `))) by A7, A13, XBOOLE_1:27;
then  (K \ L) /\ (Cl (L \ K)) = {} TS by A11, A6;
then A14: K \ L misses Cl (L \ K) by XBOOLE_0:def_7;
 Cl (K /\ (L `)) c= (Cl K) /\ (Cl (L `)) by PRE_TOPC:21;
then  (Cl (K \ L)) /\ (L \ K) c= ((Cl K) /\ (Cl (L `))) /\ (L /\ (K `)) by A7, A13, XBOOLE_1:27;
then  (Cl (K \ L)) /\ (L \ K) = {} TS by A12, A10, A9;
then  Cl (K \ L) misses L \ K by XBOOLE_0:def_7;
hence  K \ L,L \ K are_separated by A14, Def1; ::_thesis: verum
end;
A15: now__::_thesis:_for_K,_L_being_Subset_of_TS_st_K_is_closed_&_L_is_closed_holds_
K_\_L,L_\_K_are_separated
let K, L be Subset of TS; ::_thesis: ( K is closed & L is closed implies K \ L,L \ K are_separated )
assume that
A16: K is closed and
A17: L is closed ; ::_thesis: K \ L,L \ K are_separated
A18: ([#] TS) \ L is open by A17, PRE_TOPC:def_3;
A19: (([#] TS) \ K) \ (([#] TS) \ L) = (K `) /\ ((([#] TS) \ L) `) by SUBSET_1:13
.= (K `) /\ L by PRE_TOPC:3
.= L \ K by SUBSET_1:13 ;
A20: (([#] TS) \ L) \ (([#] TS) \ K) = (L `) /\ ((([#] TS) \ K) `) by SUBSET_1:13
.= (L `) /\ K by PRE_TOPC:3
.= K \ L by SUBSET_1:13 ;
 ([#] TS) \ K is open by A16, PRE_TOPC:def_3;
hence  K \ L,L \ K are_separated by A1, A18, A20, A19; ::_thesis: verum
end;
assume  ( ( K is closed & L is closed ) or ( K is open & L is open ) ) ; ::_thesis: K \ L,L \ K are_separated
hence  K \ L,L \ K are_separated by A1, A15; ::_thesis: verum
end;

definition
let GX be TopStruct ;
attrGX is connected  means :Def2: :: CONNSP_1:def 2
 for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds
B = {} GX;
end;

:: deftheorem Def2 defines connected CONNSP_1:def_2_:_
 for GX being TopStruct holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds
B = {} GX );

theorem Th10: :: CONNSP_1:10
for GX being TopSpace holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B )
proof
let GX be TopSpace; ::_thesis: ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B )
A1: now__::_thesis:_(_not_GX_is_connected_implies_ex_A,_B_being_Subset_of_GX_st_
(_[#]_GX_=_A_\/_B_&_A_<>_{}_GX_&_B_<>_{}_GX_&_A_is_closed_&_B_is_closed_&_A_misses_B_)_)
assume  not GX is connected ; ::_thesis: ex A, B being Subset of GX st
( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed & A misses B )
then consider P, Q being Subset of GX such that
A2: [#] GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {} GX and
A5: Q <> {} GX by Def2;
A6: Q is closed by A2, A3, Th4;
 P is closed by A2, A3, Th4;
hence  ex A, B being Subset of GX st
( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed & A misses B ) by A2, A3, A4, A5, A6, Th1; ::_thesis: verum
end;
now__::_thesis:_(_ex_A,_B_being_Subset_of_GX_st_
(_[#]_GX_=_A_\/_B_&_A_<>_{}_GX_&_B_<>_{}_GX_&_A_is_closed_&_B_is_closed_&_A_misses_B_)_implies_not_GX_is_connected_)
given A, B being Subset of GX such that A7: [#] GX = A \/ B and
A8: A <> {} GX and
A9: B <> {} GX and
A10: A is closed and
A11: B is closed and
A12: A misses B ; ::_thesis: not GX is connected
 A,B are_separated by A10, A11, A12, Th2;
hence  not GX is connected by A7, A8, A9, Def2; ::_thesis: verum
end;
hence  ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B ) by A1; ::_thesis: verum
end;

theorem :: CONNSP_1:11
for GX being TopSpace holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B )
proof
let GX be TopSpace; ::_thesis: ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B )
A1: now__::_thesis:_(_not_GX_is_connected_implies_ex_A,_B_being_Subset_of_GX_st_
(_[#]_GX_=_A_\/_B_&_A_<>_{}_GX_&_B_<>_{}_GX_&_A_is_open_&_B_is_open_&_A_misses_B_)_)
assume  not GX is connected ; ::_thesis: ex A, B being Subset of GX st
( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B )
then consider P, Q being Subset of GX such that
A2: [#] GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {} GX and
A5: Q <> {} GX by Def2;
reconsider P = P, Q = Q as Subset of GX ;
A6: Q is open by A2, A3, Th4;
 P is open by A2, A3, Th4;
hence  ex A, B being Subset of GX st
( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) by A2, A3, A4, A5, A6, Th1; ::_thesis: verum
end;
now__::_thesis:_(_ex_A,_B_being_Subset_of_GX_st_
(_[#]_GX_=_A_\/_B_&_A_<>_{}_GX_&_B_<>_{}_GX_&_A_is_open_&_B_is_open_&_A_misses_B_)_implies_not_GX_is_connected_)
given A, B being Subset of GX such that A7: [#] GX = A \/ B and
A8: A <> {} GX and
A9: B <> {} GX and
A10: A is open and
A11: B is open and
A12: A misses B ; ::_thesis: not GX is connected
 A,B are_separated by A7, A10, A11, A12, Th3;
hence  not GX is connected by A7, A8, A9, Def2; ::_thesis: verum
end;
hence  ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B ) by A1; ::_thesis: verum
end;

theorem Th12: :: CONNSP_1:12
for GX being TopSpace holds
( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds
Cl A meets Cl (([#] GX) \ A) )
proof
let GX be TopSpace; ::_thesis: ( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds
Cl A meets Cl (([#] GX) \ A) )
A1: now__::_thesis:_(_ex_A_being_Subset_of_GX_st_
(_A_<>_{}_GX_&_A_<>_[#]_GX_&_Cl_A_misses_Cl_(([#]_GX)_\_A)_)_implies_not_GX_is_connected_)
given A being Subset of GX such that A2: A <> {} GX and
A3: A <> [#] GX and
A4: Cl A misses Cl (([#] GX) \ A) ; ::_thesis: not GX is connected
A5: (Cl A) /\ (Cl (([#] GX) \ A)) = {} by A4, XBOOLE_0:def_7;
 A c= Cl A by PRE_TOPC:18;
then  A /\ (Cl (([#] GX) \ A)) = {} GX by A5, XBOOLE_1:3, XBOOLE_1:27;
then A6: A misses Cl (([#] GX) \ A) by XBOOLE_0:def_7;
A7: [#] GX = A \/ (A `) by PRE_TOPC:2;
A8: ([#] GX) \ A <> {} GX by A3, PRE_TOPC:4;
 ([#] GX) \ A c= Cl (([#] GX) \ A) by PRE_TOPC:18;
then  (Cl A) /\ (([#] GX) \ A) = {} by A5, XBOOLE_1:3, XBOOLE_1:27;
then  Cl A misses ([#] GX) \ A by XBOOLE_0:def_7;
then  A,([#] GX) \ A are_separated by A6, Def1;
hence  not GX is connected by A2, A8, A7, Def2; ::_thesis: verum
end;
now__::_thesis:_(_not_GX_is_connected_implies_ex_A_being_Subset_of_GX_st_
(_A_<>_{}_GX_&_A_<>_[#]_GX_&_Cl_A_misses_Cl_(([#]_GX)_\_A)_)_)
assume  not GX is connected ; ::_thesis: ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) )
then consider A, B being Subset of GX such that
A9: [#] GX = A \/ B and
A10: A <> {} GX and
A11: B <> {} GX and
A12: A is closed and
A13: B is closed and
A14: A misses B by Th10;
A15: Cl A = A by A12, PRE_TOPC:22;
A16: Cl B = B by A13, PRE_TOPC:22;
A17: B = ([#] GX) \ A by A9, A14, PRE_TOPC:5;
then  A <> [#] GX by A11, PRE_TOPC:4;
hence  ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) ) by A10, A14, A17, A15, A16; ::_thesis: verum
end;
hence  ( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds
Cl A meets Cl (([#] GX) \ A) ) by A1; ::_thesis: verum
end;

theorem :: CONNSP_1:13
for GX being TopSpace holds
( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX )
proof
let GX be TopSpace; ::_thesis: ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX )
A1: now__::_thesis:_(_not_GX_is_connected_implies_ex_P_being_Subset_of_GX_st_
(_P_is_open_&_P_is_closed_&_P_<>_{}_GX_&_P_<>_[#]_GX_)_)
assume  not GX is connected ; ::_thesis: ex P being Subset of GX st
( P is open & P is closed & P <> {} GX & P <> [#] GX )
then consider P, Q being Subset of GX such that
A2: [#] GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {} GX and
A5: Q <> {} GX by Def2;
reconsider P = P, Q = Q as Subset of GX ;
 Q = ([#] GX) \ P by A2, A3, Th1, PRE_TOPC:5;
then A6: P <> [#] GX by A5, PRE_TOPC:4;
 ( P is open & P is closed ) by A2, A3, Th4;
hence  ex P being Subset of GX st
( P is open & P is closed & P <> {} GX & P <> [#] GX ) by A4, A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_A1_being_Subset_of_GX_st_
(_A1_is_open_&_A1_is_closed_&_A1_<>_{}_GX_&_A1_<>_[#]_GX_)_implies_not_GX_is_connected_)
given A1 being Subset of GX such that A7: ( A1 is open & A1 is closed ) and
A8: A1 <> {} GX and
A9: A1 <> [#] GX ; ::_thesis: not GX is connected
A10: Cl (([#] GX) \ A1) = ([#] GX) \ A1 by A7, PRE_TOPC:23;
A11: A1 misses A1 ` by XBOOLE_1:79;
 Cl A1 = A1 by A7, PRE_TOPC:22;
hence  not GX is connected by A8, A9, A10, A11, Th12; ::_thesis: verum
end;
hence  ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX ) by A1; ::_thesis: verum
end;

theorem :: CONNSP_1:14
for GX, GY being TopSpace
for F being Function of GX,GY st F is continuous & F .: ([#] GX) = [#] GY & GX is connected holds
GY is connected
proof
let GX, GY be TopSpace; ::_thesis: for F being Function of GX,GY st F is continuous & F .: ([#] GX) = [#] GY & GX is connected holds
GY is connected
let F be Function of GX,GY; ::_thesis: ( F is continuous & F .: ([#] GX) = [#] GY & GX is connected implies GY is connected )
assume that
A1: F is continuous and
A2: F .: ([#] GX) = [#] GY and
A3: GX is connected ; ::_thesis: GY is connected
assume  not GY is connected ; ::_thesis: contradiction
then consider A, B being Subset of GY such that
A4: [#] GY = A \/ B and
A5: A <> {} GY and
A6: B <> {} GY and
A7: A is closed and
A8: B is closed and
A9: A misses B by Th10;
A10: F " A is closed by A1, A7, PRE_TOPC:def_6;
A11: F " B is closed by A1, A8, PRE_TOPC:def_6;
A12: A /\ B = {} by A9, XBOOLE_0:def_7;
(F " A) /\ (F " B) = F " (A /\ B) by FUNCT_1:68
.= {} by A12 ;
then A13: F " A misses F " B by XBOOLE_0:def_7;
 not the carrier of GY is empty by A5;
then A14: [#] GX = F " the carrier of GY by FUNCT_2:40
.= (F " A) \/ (F " B) by A4, RELAT_1:140 ;
A15: rng F = F .: the carrier of GX by RELSET_1:22;
then A16: F " B <> {} GX by A2, A6, RELAT_1:139;
 F " A <> {} GX by A2, A5, A15, RELAT_1:139;
hence  contradiction by A3, A14, A13, A10, A11, A16, Th10; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let A be Subset of GX;
attrA is connected  means :Def3: :: CONNSP_1:def 3
GX | A is connected ;
end;

:: deftheorem Def3 defines connected CONNSP_1:def_3_:_
 for GX being TopStruct
for A being Subset of GX holds
( A is connected iff GX | A is connected );

theorem Th15: :: CONNSP_1:15
for GX being TopSpace
for A being Subset of GX holds
( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )
proof
let GX be TopSpace; ::_thesis: for A being Subset of GX holds
( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )
let A be Subset of GX; ::_thesis: ( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )
A1: [#] (GX | A) = A by PRE_TOPC:def_5;
A2: now__::_thesis:_(_not_A_is_connected_implies_ex_P1,_Q1_being_Subset_of_GX_st_
(_A_=_P1_\/_Q1_&_P1,Q1_are_separated_&_P1_<>_{}_GX_&_Q1_<>_{}_GX_)_)
assume  not A is connected ; ::_thesis: ex P1, Q1 being Subset of GX st
( A = P1 \/ Q1 & P1,Q1 are_separated & P1 <> {} GX & Q1 <> {} GX )
then  not GX | A is connected by Def3;
then consider P, Q being Subset of (GX | A) such that
A3: [#] (GX | A) = P \/ Q and
A4: P,Q are_separated and
A5: P <> {} (GX | A) and
A6: Q <> {} (GX | A) by Def2;
reconsider Q1 = Q as Subset of GX by PRE_TOPC:11;
reconsider P1 = P as Subset of GX by PRE_TOPC:11;
 P1,Q1 are_separated by A4, Th5;
hence  ex P1, Q1 being Subset of GX st
( A = P1 \/ Q1 & P1,Q1 are_separated & P1 <> {} GX & Q1 <> {} GX ) by A1, A3, A5, A6; ::_thesis: verum
end;
A7: {} (GX | A) = {} ;
now__::_thesis:_(_ex_P,_Q_being_Subset_of_GX_st_
(_A_=_P_\/_Q_&_P,Q_are_separated_&_P_<>_{}_GX_&_Q_<>_{}_GX_)_implies_not_A_is_connected_)
given P, Q being Subset of GX such that A8: A = P \/ Q and
A9: P,Q are_separated and
A10: P <> {} GX and
A11: Q <> {} GX ; ::_thesis: not A is connected
reconsider Q1 = Q as Subset of (GX | A) by A1, A8, XBOOLE_1:7;
reconsider P1 = P as Subset of (GX | A) by A1, A8, XBOOLE_1:7;
 P1,Q1 are_separated by A1, A8, A9, Th6;
then  not GX | A is connected by A1, A7, A8, A10, A11, Def2;
hence  not A is connected by Def3; ::_thesis: verum
end;
hence  ( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX ) by A2; ::_thesis: verum
end;

theorem Th16: :: CONNSP_1:16
for GX being TopSpace
for A, B, C being Subset of GX st A is connected & A c= B \/ C & B,C are_separated & not A c= B holds
A c= C
proof
let GX be TopSpace; ::_thesis: for A, B, C being Subset of GX st A is connected & A c= B \/ C & B,C are_separated & not A c= B holds
A c= C
let A, B, C be Subset of GX; ::_thesis: ( A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )
assume that
A1: A is connected and
A2: A c= B \/ C and
A3: B,C are_separated ; ::_thesis: ( A c= B or A c= C )
A4: A /\ C c= C by XBOOLE_1:17;
 A /\ B c= B by XBOOLE_1:17;
then A5: A /\ B,A /\ C are_separated by A3, A4, Th7;
A6: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
.= A by A2, XBOOLE_1:28 ;
assume that
A7: not A c= B and
A8: not A c= C ; ::_thesis: contradiction
 A meets C by A2, A7, XBOOLE_1:73;
then A9: A /\ C <> {} by XBOOLE_0:def_7;
 A meets B by A2, A8, XBOOLE_1:73;
then A10: A /\ B <> {} by XBOOLE_0:def_7;
then  A <> {} GX ;
hence  contradiction by A1, A10, A9, A5, A6, Th15; ::_thesis: verum
end;

theorem Th17: :: CONNSP_1:17
for GX being TopSpace
for A, B being Subset of GX st A is connected & B is connected & not A,B are_separated holds
A \/ B is connected
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & not A,B are_separated holds
A \/ B is connected
let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & not A,B are_separated implies A \/ B is connected )
assume that
A1: A is connected and
A2: B is connected and
A3: not A,B are_separated ; ::_thesis: A \/ B is connected
assume  not A \/ B is connected ; ::_thesis: contradiction
then consider P, Q being Subset of GX such that
A4: A \/ B = P \/ Q and
A5: P,Q are_separated and
A6: P <> {} GX and
A7: Q <> {} GX by Th15;
A8: ( not A c= Q or not B c= P ) by A3, A5, Th7;
 P misses Q by A5, Th1;
then A9: P /\ Q = {} by XBOOLE_0:def_7;
A10: now__::_thesis:_(_A_c=_P_implies_not_B_c=_P_)
A11: P c= P \/ Q by XBOOLE_1:7;
assume that
A12: A c= P and
A13: B c= P ; ::_thesis: contradiction
 A \/ B c= P by A12, A13, XBOOLE_1:8;
then  P \/ Q = P by A4, A11, XBOOLE_0:def_10;
hence  contradiction by A7, A9, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;
A14: now__::_thesis:_(_A_c=_Q_implies_not_B_c=_Q_)
A15: Q c= Q \/ P by XBOOLE_1:7;
assume that
A16: A c= Q and
A17: B c= Q ; ::_thesis: contradiction
 A \/ B c= Q by A16, A17, XBOOLE_1:8;
then  Q \/ P = Q by A4, A15, XBOOLE_0:def_10;
hence  contradiction by A6, A9, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;
 ( not A c= P or not B c= Q ) by A3, A5, Th7;
hence  contradiction by A1, A2, A4, A5, A10, A8, A14, Th16, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th18: :: CONNSP_1:18
for GX being TopSpace
for C, A being Subset of GX st C is connected & C c= A & A c= Cl C holds
A is connected
proof
let GX be TopSpace; ::_thesis: for C, A being Subset of GX st C is connected & C c= A & A c= Cl C holds
A is connected
let C, A be Subset of GX; ::_thesis: ( C is connected & C c= A & A c= Cl C implies A is connected )
assume that
A1: C is connected and
A2: C c= A and
A3: A c= Cl C ; ::_thesis: A is connected
assume  not A is connected ; ::_thesis: contradiction
then consider P, Q being Subset of GX such that
A4: A = P \/ Q and
A5: P,Q are_separated and
A6: P <> {} GX and
A7: Q <> {} GX by Th15;
 P misses Cl Q by A5, Def1;
then A8: P /\ (Cl Q) = {} by XBOOLE_0:def_7;
A9: now__::_thesis:_not_C_c=_Q
assume  C c= Q ; ::_thesis: contradiction
then  Cl C c= Cl Q by PRE_TOPC:19;
then  P /\ (Cl C) = {} by A8, XBOOLE_1:3, XBOOLE_1:27;
then  P /\ A = {} by A3, XBOOLE_1:3, XBOOLE_1:27;
hence  contradiction by A4, A6, XBOOLE_1:21; ::_thesis: verum
end;
 Cl P misses Q by A5, Def1;
then A10: (Cl P) /\ Q = {} by XBOOLE_0:def_7;
now__::_thesis:_not_C_c=_P
assume  C c= P ; ::_thesis: contradiction
then  Cl C c= Cl P by PRE_TOPC:19;
then  (Cl C) /\ Q = {} by A10, XBOOLE_1:3, XBOOLE_1:27;
then  A /\ Q = {} by A3, XBOOLE_1:3, XBOOLE_1:27;
hence  contradiction by A4, A7, XBOOLE_1:21; ::_thesis: verum
end;
hence  contradiction by A1, A2, A4, A5, A9, Th16; ::_thesis: verum
end;

theorem Th19: :: CONNSP_1:19
for GX being TopSpace
for A being Subset of GX st A is connected holds
Cl A is connected
proof
let GX be TopSpace; ::_thesis: for A being Subset of GX st A is connected holds
Cl A is connected
let A be Subset of GX; ::_thesis: ( A is connected implies Cl A is connected )
A1: A c= Cl A by PRE_TOPC:18;
assume  A is connected ; ::_thesis: Cl A is connected
hence  Cl A is connected by A1, Th18; ::_thesis: verum
end;

theorem Th20: :: CONNSP_1:20
for GX being TopSpace
for A, B, C being Subset of GX st GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated holds
( A \/ B is connected & A \/ C is connected )
proof
let GX be TopSpace; ::_thesis: for A, B, C being Subset of GX st GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated holds
( A \/ B is connected & A \/ C is connected )
let A, B, C be Subset of GX; ::_thesis: ( GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated implies ( A \/ B is connected & A \/ C is connected ) )
assume that
A1: GX is connected and
A2: A is connected and
A3: ([#] GX) \ A = B \/ C and
A4: B,C are_separated ; ::_thesis: ( A \/ B is connected & A \/ C is connected )
now__::_thesis:_for_A,_B,_C_being_Subset_of_GX_st_GX_is_connected_&_A_is_connected_&_([#]_GX)_\_A_=_B_\/_C_&_B,C_are_separated_holds_
A_\/_B_is_connected
let A, B, C be Subset of GX; ::_thesis: ( GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated implies A \/ B is connected )
assume that
A5: GX is connected and
A6: A is connected and
A7: ([#] GX) \ A = B \/ C and
A8: B,C are_separated ; ::_thesis: A \/ B is connected
now__::_thesis:_for_P,_Q_being_Subset_of_GX_st_A_\/_B_=_P_\/_Q_&_P,Q_are_separated_&_not_P_=_{}_GX_holds_
Q_=_{}_GX
let P, Q be Subset of GX; ::_thesis: ( A \/ B = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )
assume that
A9: A \/ B = P \/ Q and
A10: P,Q are_separated ; ::_thesis: ( P = {} GX or Q = {} GX )
A11: [#] GX = A \/ (B \/ C) by A7, XBOOLE_1:45
.= (P \/ Q) \/ C by A9, XBOOLE_1:4 ;
A12: now__::_thesis:_(_not_A_c=_Q_or_P_=_{}_GX_or_Q_=_{}_GX_)
assume  A c= Q ; ::_thesis: ( P = {} GX or Q = {} GX )
then  P misses A by A10, Th1, Th7;
then  P c= B by A9, XBOOLE_1:7, XBOOLE_1:73;
then  P,C are_separated by A8, Th7;
then A13: P,Q \/ C are_separated by A10, Th8;
 [#] GX = P \/ (Q \/ C) by A11, XBOOLE_1:4;
hence  ( P = {} GX or Q = {} GX ) by A5, A13, Def2; ::_thesis: verum
end;
now__::_thesis:_(_not_A_c=_P_or_P_=_{}_GX_or_Q_=_{}_GX_)
assume  A c= P ; ::_thesis: ( P = {} GX or Q = {} GX )
then  Q misses A by A10, Th1, Th7;
then  Q c= B by A9, XBOOLE_1:7, XBOOLE_1:73;
then  Q,C are_separated by A8, Th7;
then A14: Q,P \/ C are_separated by A10, Th8;
 [#] GX = Q \/ (P \/ C) by A11, XBOOLE_1:4;
hence  ( P = {} GX or Q = {} GX ) by A5, A14, Def2; ::_thesis: verum
end;
hence  ( P = {} GX or Q = {} GX ) by A6, A9, A10, A12, Th16, XBOOLE_1:7; ::_thesis: verum
end;
hence  A \/ B is connected by Th15; ::_thesis: verum
end;
hence  ( A \/ B is connected & A \/ C is connected ) by A1, A2, A3, A4; ::_thesis: verum
end;

theorem :: CONNSP_1:21
for GX being TopSpace
for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds
( A \/ B is closed & A \/ C is closed )
proof
let GX be TopSpace; ::_thesis: for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds
( A \/ B is closed & A \/ C is closed )
let A, B, C be Subset of GX; ::_thesis: ( ([#] GX) \ A = B \/ C & B,C are_separated & A is closed implies ( A \/ B is closed & A \/ C is closed ) )
assume that
A1: ([#] GX) \ A = B \/ C and
A2: B,C are_separated and
A3: A is closed ; ::_thesis: ( A \/ B is closed & A \/ C is closed )
now__::_thesis:_for_A,_B,_C_being_Subset_of_GX_st_([#]_GX)_\_A_=_B_\/_C_&_B,C_are_separated_&_A_is_closed_holds_
A_\/_B_is_closed
let A, B, C be Subset of GX; ::_thesis: ( ([#] GX) \ A = B \/ C & B,C are_separated & A is closed implies A \/ B is closed )
assume that
A4: ([#] GX) \ A = B \/ C and
A5: B,C are_separated and
A6: A is closed ; ::_thesis: A \/ B is closed
A7: Cl A = A by A6, PRE_TOPC:22;
 Cl B misses C by A5, Def1;
then A8: (Cl B) /\ C = {} by XBOOLE_0:def_7;
A9: [#] GX = A \/ (B \/ C) by A4, XBOOLE_1:45;
Cl (A \/ B) = (Cl A) \/ (Cl B) by PRE_TOPC:20
.= A \/ ((Cl B) /\ (A \/ (B \/ C))) by A7, A9, XBOOLE_1:28
.= (A \/ (Cl B)) /\ (A \/ (A \/ (B \/ C))) by XBOOLE_1:24
.= (A \/ (Cl B)) /\ ((A \/ A) \/ (B \/ C)) by XBOOLE_1:4
.= A \/ ((Cl B) /\ (B \/ C)) by XBOOLE_1:24
.= A \/ (((Cl B) /\ B) \/ ((Cl B) /\ C)) by XBOOLE_1:23
.= A \/ B by A8, PRE_TOPC:18, XBOOLE_1:28 ;
hence  A \/ B is closed by PRE_TOPC:22; ::_thesis: verum
end;
hence  ( A \/ B is closed & A \/ C is closed ) by A1, A2, A3; ::_thesis: verum
end;

theorem :: CONNSP_1:22
for GX being TopSpace
for C, A being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds
C meets Fr A
proof
let GX be TopSpace; ::_thesis: for C, A being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds
C meets Fr A
let C, A be Subset of GX; ::_thesis: ( C is connected & C meets A & C \ A <> {} GX implies C meets Fr A )
assume that
A1: C is connected and
A2: C meets A and
A3: C \ A <> {} GX ; ::_thesis: C meets Fr A
A4: A ` c= Cl (A `) by PRE_TOPC:18;
 Cl (C /\ A) c= Cl A by PRE_TOPC:19, XBOOLE_1:17;
then A5: (Cl (C /\ A)) /\ (A `) c= (Cl A) /\ (Cl (A `)) by A4, XBOOLE_1:27;
A6: A c= Cl A by PRE_TOPC:18;
A7: C \ A = C /\ (A `) by SUBSET_1:13;
then  Cl (C \ A) c= Cl (A `) by PRE_TOPC:19, XBOOLE_1:17;
then  A /\ (Cl (C /\ (A `))) c= (Cl A) /\ (Cl (A `)) by A7, A6, XBOOLE_1:27;
then  ((Cl (C /\ A)) /\ (A `)) \/ (A /\ (Cl (C /\ (A `)))) c= (Cl A) /\ (Cl (A `)) by A5, XBOOLE_1:8;
then A8: C /\ (((Cl (C /\ A)) /\ (A `)) \/ (A /\ (Cl (C /\ (A `))))) c= C /\ ((Cl A) /\ (Cl (A `))) by XBOOLE_1:27;
A9: C = C /\ ([#] GX) by XBOOLE_1:28
.= C /\ (A \/ (A `)) by PRE_TOPC:2
.= (C /\ A) \/ (C \ A) by A7, XBOOLE_1:23 ;
 C /\ A <> {} by A2, XBOOLE_0:def_7;
then  not C /\ A,C \ A are_separated by A1, A3, A9, Th15;
then  ( Cl (C /\ A) meets C \ A or C /\ A meets Cl (C \ A) ) by Def1;
then A10: ( (Cl (C /\ A)) /\ (C \ A) <> {} or (C /\ A) /\ (Cl (C \ A)) <> {} ) by XBOOLE_0:def_7;
((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) = (((Cl (C /\ A)) /\ C) /\ (A `)) \/ ((C /\ A) /\ (Cl (C /\ (A `)))) by A7, XBOOLE_1:16
.= ((C /\ (Cl (C /\ A))) /\ (A `)) \/ (C /\ (A /\ (Cl (C /\ (A `))))) by XBOOLE_1:16
.= (C /\ ((Cl (C /\ A)) /\ (A `))) \/ (C /\ (A /\ (Cl (C /\ (A `))))) by XBOOLE_1:16
.= C /\ (((Cl (C /\ A)) /\ (A `)) \/ (A /\ (Cl (C /\ (A `))))) by XBOOLE_1:23 ;
then  ((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) c= C /\ (Fr A) by A8, TOPS_1:def_2;
hence  C /\ (Fr A) <> {} by A10; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th23: :: CONNSP_1:23
for GX being TopSpace
for X9 being SubSpace of GX
for A being Subset of GX
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
proof
let GX be TopSpace; ::_thesis: for X9 being SubSpace of GX
for A being Subset of GX
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let X9 be SubSpace of GX; ::_thesis: for A being Subset of GX
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let A be Subset of GX; ::_thesis: for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let B be Subset of X9; ::_thesis: ( A = B implies ( A is connected iff B is connected ) )
assume A1: A = B ; ::_thesis: ( A is connected iff B is connected )
reconsider GX9 = GX, X = X9 as TopSpace ;
A2: [#] (GX | A) = A by PRE_TOPC:def_5;
reconsider B9 = B as Subset of X ;
reconsider A9 = A as Subset of GX9 ;
A3: [#] (X9 | B) = B by PRE_TOPC:def_5;
A4: {} (GX | A) = {} (X9 | B) ;
A5: now__::_thesis:_(_not_A_is_connected_implies_not_B_is_connected_)
assume  not A is connected ; ::_thesis: not B is connected
then  not GX9 | A9 is connected by Def3;
then consider P, Q being Subset of (GX | A) such that
A6: [#] (GX | A) = P \/ Q and
A7: P <> {} (GX | A) and
A8: Q <> {} (GX | A) and
A9: P is closed and
A10: Q is closed and
A11: P misses Q by Th10;
consider P1 being Subset of GX such that
A12: P1 is closed and
A13: P1 /\ ([#] (GX | A)) = P by A9, PRE_TOPC:13;
reconsider P11 = P1 /\ ([#] X9) as Subset of X9 ;
A14: P11 is closed by A12, PRE_TOPC:13;
reconsider PP = P, QQ = Q as Subset of (X9 | B) by A1, A2, A3;
A15: P c= [#] X9 by A1, A2, XBOOLE_1:1;
 P1 /\ A c= P1 by XBOOLE_1:17;
then  P c= P1 /\ ([#] X9) by A2, A13, A15, XBOOLE_1:19;
then A16: P c= (P1 /\ ([#] X9)) /\ A by A2, XBOOLE_1:19;
 P1 /\ ([#] X9) c= P1 by XBOOLE_1:17;
then  (P1 /\ ([#] X9)) /\ A c= P by A2, A13, XBOOLE_1:27;
then  P11 /\ ([#] (X9 | B)) = PP by A1, A3, A16, XBOOLE_0:def_10;
then A17: PP is closed by A14, PRE_TOPC:13;
consider Q1 being Subset of GX such that
A18: Q1 is closed and
A19: Q1 /\ ([#] (GX | A)) = Q by A10, PRE_TOPC:13;
reconsider Q11 = Q1 /\ ([#] X9) as Subset of X9 ;
A20: Q c= [#] X9 by A1, A2, XBOOLE_1:1;
 Q1 /\ A c= Q1 by XBOOLE_1:17;
then  Q c= Q1 /\ ([#] X9) by A2, A19, A20, XBOOLE_1:19;
then A21: Q c= (Q1 /\ ([#] X9)) /\ A by A2, XBOOLE_1:19;
 Q1 /\ ([#] X9) c= Q1 by XBOOLE_1:17;
then  (Q1 /\ ([#] X9)) /\ A c= Q by A2, A19, XBOOLE_1:27;
then A22: (Q1 /\ ([#] X9)) /\ A = Q by A21, XBOOLE_0:def_10;
 Q11 is closed by A18, PRE_TOPC:13;
then  QQ is closed by A1, A3, A22, PRE_TOPC:13;
then  not X | B9 is connected by A1, A2, A3, A4, A6, A7, A8, A11, A17, Th10;
hence  not B is connected by Def3; ::_thesis: verum
end;
now__::_thesis:_(_not_B_is_connected_implies_not_A_is_connected_)
assume  not B is connected ; ::_thesis: not A is connected
then  not X9 | B is connected by Def3;
then consider P, Q being Subset of (X9 | B) such that
A23: [#] (X9 | B) = P \/ Q and
A24: P <> {} (X9 | B) and
A25: Q <> {} (X9 | B) and
A26: P is closed and
A27: Q is closed and
A28: P misses Q by Th10;
reconsider QQ = Q as Subset of (GX | A) by A1, A2, A3;
reconsider PP = P as Subset of (GX | A) by A1, A2, A3;
consider P1 being Subset of X9 such that
A29: P1 is closed and
A30: P1 /\ ([#] (X9 | B)) = P by A26, PRE_TOPC:13;
consider Q1 being Subset of X9 such that
A31: Q1 is closed and
A32: Q1 /\ ([#] (X9 | B)) = Q by A27, PRE_TOPC:13;
consider Q2 being Subset of GX such that
A33: Q2 is closed and
A34: Q2 /\ ([#] X9) = Q1 by A31, PRE_TOPC:13;
Q2 /\ ([#] (GX | A)) = Q2 /\ (([#] X9) /\ B) by A1, A2, XBOOLE_1:28
.= QQ by A3, A32, A34, XBOOLE_1:16 ;
then A35: QQ is closed by A33, PRE_TOPC:13;
consider P2 being Subset of GX such that
A36: P2 is closed and
A37: P2 /\ ([#] X9) = P1 by A29, PRE_TOPC:13;
P2 /\ ([#] (GX | A)) = P2 /\ (([#] X9) /\ B) by A1, A2, XBOOLE_1:28
.= PP by A3, A30, A37, XBOOLE_1:16 ;
then  PP is closed by A36, PRE_TOPC:13;
then  not GX9 | A9 is connected by A1, A2, A3, A4, A23, A24, A25, A28, A35, Th10;
hence  not A is connected by Def3; ::_thesis: verum
end;
hence  ( A is connected iff B is connected ) by A5; ::_thesis: verum
end;

theorem :: CONNSP_1:24
for GX being TopSpace
for A, B being Subset of GX st A is closed & B is closed & A \/ B is connected & A /\ B is connected holds
( A is connected & B is connected )
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX st A is closed & B is closed & A \/ B is connected & A /\ B is connected holds
( A is connected & B is connected )
let A, B be Subset of GX; ::_thesis: ( A is closed & B is closed & A \/ B is connected & A /\ B is connected implies ( A is connected & B is connected ) )
assume that
A1: A is closed and
A2: B is closed ; ::_thesis: ( not A \/ B is connected or not A /\ B is connected or ( A is connected & B is connected ) )
set AB = A \/ B;
A3: A \/ B = [#] (GX | (A \/ B)) by PRE_TOPC:def_5;
then reconsider B1 = B as Subset of (GX | (A \/ B)) by XBOOLE_1:7;
reconsider A1 = A as Subset of (GX | (A \/ B)) by A3, XBOOLE_1:7;
A4: ([#] (GX | (A \/ B))) \ (A1 /\ B1) = (A1 \ B1) \/ (B1 \ A1) by A3, XBOOLE_1:55;
 B /\ ([#] (GX | (A \/ B))) = B by A3, XBOOLE_1:7, XBOOLE_1:28;
then A5: B1 is closed by A2, PRE_TOPC:13;
 A /\ ([#] (GX | (A \/ B))) = A by A3, XBOOLE_1:7, XBOOLE_1:28;
then  A1 is closed by A1, PRE_TOPC:13;
then A6: A1 \ B1,B1 \ A1 are_separated by A5, Th9;
assume that
A7: A \/ B is connected and
A8: A /\ B is connected ; ::_thesis: ( A is connected & B is connected )
A9: GX | (A \/ B) is connected by A7, Def3;
A10: A1 /\ B1 is connected by A8, Th23;
 (A1 /\ B1) \/ (B1 \ A1) = B1 by XBOOLE_1:51;
then A11: B1 is connected by A9, A4, A6, A10, Th20;
 (A1 /\ B1) \/ (A1 \ B1) = A1 by XBOOLE_1:51;
then  A1 is connected by A9, A4, A6, A10, Th20;
hence  ( A is connected & B is connected ) by A11, Th23; ::_thesis: verum
end;

theorem Th25: :: CONNSP_1:25
for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & ex A being Subset of GX st
( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds
not A,B are_separated ) ) holds
union F is connected
proof
let GX be TopSpace; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & ex A being Subset of GX st
( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds
not A,B are_separated ) ) holds
union F is connected
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in F holds
A is connected ) & ex A being Subset of GX st
( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds
not A,B are_separated ) ) implies union F is connected )
assume that
A1: for A being Subset of GX st A in F holds
A is connected and
A2: ex A being Subset of GX st
( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds
not A,B are_separated ) ) ; ::_thesis: union F is connected
consider A1 being Subset of GX such that
 A1 <> {} GX and
A3: A1 in F and
A4: for B being Subset of GX st B in F & B <> A1 holds
not A1,B are_separated by A2;
reconsider A1 = A1 as Subset of GX ;
now__::_thesis:_for_P,_Q_being_Subset_of_GX_st_union_F_=_P_\/_Q_&_P,Q_are_separated_&_not_P_=_{}_GX_holds_
Q_=_{}_GX
let P, Q be Subset of GX; ::_thesis: ( union F = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )
assume that
A5: union F = P \/ Q and
A6: P,Q are_separated ; ::_thesis: ( P = {} GX or Q = {} GX )
 P misses Q by A6, Th1;
then A7: P /\ Q = {} by XBOOLE_0:def_7;
A8: now__::_thesis:_(_A1_c=_Q_implies_P_=_{}_GX_)
assume A9: A1 c= Q ; ::_thesis: P = {} GX
now__::_thesis:_for_B_being_Subset_of_GX_st_B_in_F_&_B_<>_A1_holds_
B_c=_Q
let B be Subset of GX; ::_thesis: ( B in F & B <> A1 implies B c= Q )
assume that
A10: B in F and
 B <> A1 and
A11: not B c= Q ; ::_thesis: contradiction
 B is connected by A1, A10;
then  ( B c= P or B c= Q ) by A5, A6, A10, Th16, ZFMISC_1:74;
hence  contradiction by A4, A6, A9, A10, A11, Th7; ::_thesis: verum
end;
then  for A being set st A in F holds
A c= Q by A9;
then A12: union F c= Q by ZFMISC_1:76;
 Q c= P \/ Q by XBOOLE_1:7;
then  Q = P \/ Q by A5, A12, XBOOLE_0:def_10;
hence  P = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;
A13: now__::_thesis:_(_A1_c=_P_implies_Q_=_{}_GX_)
assume A14: A1 c= P ; ::_thesis: Q = {} GX
now__::_thesis:_for_B_being_Subset_of_GX_st_B_in_F_&_B_<>_A1_holds_
B_c=_P
let B be Subset of GX; ::_thesis: ( B in F & B <> A1 implies B c= P )
assume that
A15: B in F and
 B <> A1 ; ::_thesis: B c= P
 B is connected by A1, A15;
then A16: ( B c= P or B c= Q ) by A5, A6, A15, Th16, ZFMISC_1:74;
assume  not B c= P ; ::_thesis: contradiction
hence  contradiction by A4, A6, A14, A15, A16, Th7; ::_thesis: verum
end;
then  for A being set st A in F holds
A c= P by A14;
then A17: union F c= P by ZFMISC_1:76;
 P c= P \/ Q by XBOOLE_1:7;
then  P = P \/ Q by A5, A17, XBOOLE_0:def_10;
hence  Q = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;
 A1 c= P \/ Q by A3, A5, ZFMISC_1:74;
hence  ( P = {} GX or Q = {} GX ) by A1, A3, A6, A13, A8, Th16; ::_thesis: verum
end;
hence  union F is connected by Th15; ::_thesis: verum
end;

theorem Th26: :: CONNSP_1:26
for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & meet F <> {} GX holds
union F is connected
proof
let GX be TopSpace; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & meet F <> {} GX holds
union F is connected
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in F holds
A is connected ) & meet F <> {} GX implies union F is connected )
assume that
A1: for A being Subset of GX st A in F holds
A is connected and
A2: meet F <> {} GX ; ::_thesis: union F is connected
consider x being Point of GX such that
A3: x in meet F by A2, PRE_TOPC:12;
 meet F c= union F by SETFAM_1:2;
then consider A2 being set  such that
A4: x in A2 and
A5: A2 in F by A3, TARSKI:def_4;
reconsider A2 = A2 as Subset of GX by A5;
A6: now__::_thesis:_for_B_being_Subset_of_GX_st_B_in_F_&_B_<>_A2_holds_
not_A2,B_are_separated
let B be Subset of GX; ::_thesis: ( B in F & B <> A2 implies not A2,B are_separated )
assume that
A7: B in F and
 B <> A2 ; ::_thesis: not A2,B are_separated
 A2 c= Cl A2 by PRE_TOPC:18;
then  ( ( x in Cl A2 & x in B ) or ( x in A2 & x in Cl B ) ) by A3, A4, A7, SETFAM_1:def_1;
then  ( (Cl A2) /\ B <> {} or A2 /\ (Cl B) <> {} ) by XBOOLE_0:def_4;
then  ( Cl A2 meets B or A2 meets Cl B ) by XBOOLE_0:def_7;
hence  not A2,B are_separated by Def1; ::_thesis: verum
end;
 A2 <> {} GX by A4;
hence  union F is connected by A1, A5, A6, Th25; ::_thesis: verum
end;

theorem Th27: :: CONNSP_1:27
for GX being TopSpace holds
( [#] GX is connected iff GX is connected )
proof
let GX be TopSpace; ::_thesis: ( [#] GX is connected iff GX is connected )
A1: [#] GX = [#] (GX | ([#] GX)) by PRE_TOPC:def_5;
A2: {} (GX | ([#] GX)) = {} GX ;
A3: now__::_thesis:_(_GX_is_connected_implies_[#]_GX_is_connected_)
assume A4: GX is connected ; ::_thesis: [#] GX is connected
now__::_thesis:_for_P1,_Q1_being_Subset_of_(GX_|_([#]_GX))_st_[#]_(GX_|_([#]_GX))_=_P1_\/_Q1_&_P1,Q1_are_separated_&_not_P1_=_{}_(GX_|_([#]_GX))_holds_
Q1_=_{}_(GX_|_([#]_GX))
let P1, Q1 be Subset of (GX | ([#] GX)); ::_thesis: ( [#] (GX | ([#] GX)) = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} (GX | ([#] GX)) implies Q1 = {} (GX | ([#] GX)) )
assume that
A5: [#] (GX | ([#] GX)) = P1 \/ Q1 and
A6: P1,Q1 are_separated ; ::_thesis: ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) )
reconsider Q = Q1 as Subset of GX by PRE_TOPC:11;
reconsider P = P1 as Subset of GX by PRE_TOPC:11;
 P,Q are_separated by A6, Th5;
hence  ( P1 = {} (GX | ([#] GX)) or Q1 = {} (GX | ([#] GX)) ) by A2, A1, A4, A5, Def2; ::_thesis: verum
end;
then  GX | ([#] GX) is connected by Def2;
hence  [#] GX is connected by Def3; ::_thesis: verum
end;
now__::_thesis:_(_[#]_GX_is_connected_implies_GX_is_connected_)
assume  [#] GX is connected ; ::_thesis: GX is connected
then A7: GX | ([#] GX) is connected by Def3;
now__::_thesis:_for_P1,_Q1_being_Subset_of_GX_st_[#]_GX_=_P1_\/_Q1_&_P1,Q1_are_separated_&_not_P1_=_{}_GX_holds_
Q1_=_{}_GX
let P1, Q1 be Subset of GX; ::_thesis: ( [#] GX = P1 \/ Q1 & P1,Q1 are_separated & not P1 = {} GX implies Q1 = {} GX )
assume that
A8: [#] GX = P1 \/ Q1 and
A9: P1,Q1 are_separated ; ::_thesis: ( P1 = {} GX or Q1 = {} GX )
reconsider Q = Q1 as Subset of (GX | ([#] GX)) by A1;
reconsider P = P1 as Subset of (GX | ([#] GX)) by A1;
 P,Q are_separated by A1, A8, A9, Th6;
hence  ( P1 = {} GX or Q1 = {} GX ) by A2, A1, A7, A8, Def2; ::_thesis: verum
end;
hence  GX is connected by Def2; ::_thesis: verum
end;
hence  ( [#] GX is connected iff GX is connected ) by A3; ::_thesis: verum
end;

registration
let GX be non empty TopSpace;
let x be Point of GX;
cluster{x} ->  connected for Subset of GX;
coherence
 for b1 being Subset of GX st b1 = {x} holds
b1 is connected
proof
now__::_thesis:_{x}_is_connected
assume  not {x} is connected ; ::_thesis: contradiction
then consider P, Q being Subset of GX such that
A1: {x} = P \/ Q and
A2: P,Q are_separated and
A3: P <> {} GX and
A4: Q <> {} GX by Th15;
 P <> Q
proof
assume  not P <> Q ; ::_thesis: contradiction
then A5: P /\ Q = P ;
 P misses Q by A2, Th1;
hence  contradiction by A3, A5, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  contradiction by A1, A3, A4, ZFMISC_1:38; ::_thesis: verum
end;
hence  for b1 being Subset of GX st b1 = {x} holds
b1 is connected ; ::_thesis: verum
end;
end;

definition
let GX be TopStruct ;
let x, y be Point of GX;
predx,y are_joined  means :Def4: :: CONNSP_1:def 4
 ex C being Subset of GX st
( C is connected & x in C & y in C );
end;

:: deftheorem Def4 defines are_joined CONNSP_1:def_4_:_
 for GX being TopStruct
for x, y being Point of GX holds
( x,y are_joined iff ex C being Subset of GX st
( C is connected & x in C & y in C ) );

theorem Th28: :: CONNSP_1:28
for GX being non empty TopSpace st ex x being Point of GX st
for y being Point of GX holds x,y are_joined holds
GX is connected
proof
let GX be non empty TopSpace; ::_thesis: ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined implies GX is connected )
given a being Point of GX such that A1: for x being Point of GX holds a,x are_joined ; ::_thesis: GX is connected
now__::_thesis:_for_x_being_Point_of_GX_ex_F_being_Subset-Family_of_GX_st_
for_C_being_Subset_of_GX_holds_
(_(_C_in_F_implies_(_C_is_connected_&_x_in_C_)_)_&_(_C_is_connected_&_x_in_C_implies_C_in_F_)_)
let x be Point of GX; ::_thesis: ex F being Subset-Family of GX st
for C being Subset of GX holds
( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
defpred S1[ set ] means  ex C1 being Subset of GX st
( C1 = $1 & C1 is connected & x in $1 );
consider F being Subset-Family of GX such that
A2: for C being Subset of GX holds
( C in F iff S1[C] ) from SUBSET_1:sch_3();
take F = F; ::_thesis: for C being Subset of GX holds
( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
let C be Subset of GX; ::_thesis: ( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
thus  ( C in F implies ( C is connected & x in C ) ) ::_thesis: ( C is connected & x in C implies C in F )
proof
assume  C in F ; ::_thesis: ( C is connected & x in C )
then  ex C1 being Subset of GX st
( C1 = C & C1 is connected & x in C ) by A2;
hence  ( C is connected & x in C ) ; ::_thesis: verum
end;
thus  ( C is connected & x in C implies C in F ) by A2; ::_thesis: verum
end;
then consider F being Subset-Family of GX such that
A3: for C being Subset of GX holds
( C in F iff ( C is connected & a in C ) ) ;
A4: now__::_thesis:_for_x_being_Point_of_GX_ex_C_being_Subset_of_GX_st_
(_C_is_connected_&_a_in_C_&_x_in_C_)
let x be Point of GX; ::_thesis: ex C being Subset of GX st
( C is connected & a in C & x in C )
 a,x are_joined by A1;
hence  ex C being Subset of GX st
( C is connected & a in C & x in C ) by Def4; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_[#]_GX_holds_
x_in_union_F
let x be set ; ::_thesis: ( x in [#] GX implies x in union F )
assume  x in [#] GX ; ::_thesis: x in union F
then consider C being Subset of GX such that
A5: C is connected and
A6: a in C and
A7: x in C by A4;
 C in F by A3, A5, A6;
hence  x in union F by A7, TARSKI:def_4; ::_thesis: verum
end;
then  [#] GX c= union F by TARSKI:def_3;
then A8: union F = [#] GX by XBOOLE_0:def_10;
A9: for A being set st A in F holds
a in A by A3;
 a in {a} by TARSKI:def_1;
then  F <> {} by A3;
then A10: meet F <> {} GX by A9, SETFAM_1:def_1;
 for A being Subset of GX st A in F holds
A is connected by A3;
then  [#] GX is connected by A8, A10, Th26;
hence  GX is connected by Th27; ::_thesis: verum
end;

theorem Th29: :: CONNSP_1:29
for GX being TopSpace holds
( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined )
proof
let GX be TopSpace; ::_thesis: ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined )
A1: now__::_thesis:_(_ex_a_being_Point_of_GX_st_
for_x_being_Point_of_GX_holds_a,x_are_joined_implies_for_x,_y_being_Point_of_GX_holds_x,y_are_joined_)
given a being Point of GX such that A2: for x being Point of GX holds a,x are_joined ; ::_thesis: for x, y being Point of GX holds x,y are_joined
let x, y be Point of GX; ::_thesis: x,y are_joined
 a,x are_joined by A2;
then consider C1 being Subset of GX such that
A3: C1 is connected and
A4: a in C1 and
A5: x in C1 by Def4;
 a,y are_joined by A2;
then consider C2 being Subset of GX such that
A6: C2 is connected and
A7: a in C2 and
A8: y in C2 by Def4;
 C1 /\ C2 <> {} GX by A4, A7, XBOOLE_0:def_4;
then  C1 meets C2 by XBOOLE_0:def_7;
then A9: C1 \/ C2 is connected by A3, A6, Th1, Th17;
A10: y in C1 \/ C2 by A8, XBOOLE_0:def_3;
 x in C1 \/ C2 by A5, XBOOLE_0:def_3;
hence  x,y are_joined by A9, A10, Def4; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x,_y_being_Point_of_GX_holds_x,y_are_joined_)_implies_ex_x_being_Point_of_GX_st_
for_y_being_Point_of_GX_holds_x,y_are_joined_)
set a = the Point of GX;
assume  for x, y being Point of GX holds x,y are_joined ; ::_thesis: ex x being Point of GX st
for y being Point of GX holds x,y are_joined
then  for y being Point of GX holds the Point of GX,y are_joined ;
hence  ex x being Point of GX st
for y being Point of GX holds x,y are_joined ; ::_thesis: verum
end;
hence  ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined ) by A1; ::_thesis: verum
end;

theorem :: CONNSP_1:30
for GX being non empty TopSpace st ( for x, y being Point of GX holds x,y are_joined ) holds
GX is connected
proof
let GX be non empty TopSpace; ::_thesis: ( ( for x, y being Point of GX holds x,y are_joined ) implies GX is connected )
assume  for x, y being Point of GX holds x,y are_joined ; ::_thesis: GX is connected
then  ex x being Point of GX st
for y being Point of GX holds x,y are_joined by Th29;
hence  GX is connected by Th28; ::_thesis: verum
end;

theorem Th31: :: CONNSP_1:31
for GX being non empty TopSpace
for x being Point of GX
for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) holds
F <> {}
proof
let GX be non empty TopSpace; ::_thesis: for x being Point of GX
for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) holds
F <> {}
let x be Point of GX; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) holds
F <> {}
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) implies F <> {} )
assume A1: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ; ::_thesis: F <> {}
 x in {x} by TARSKI:def_1;
hence  F <> {} by A1; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let A be Subset of GX;
attrA is a_component  means :Def5: :: CONNSP_1:def 5
( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) );
end;

:: deftheorem Def5 defines a_component CONNSP_1:def_5_:_
 for GX being TopStruct
for A being Subset of GX holds
( A is a_component iff ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) ) );

registration
let GX be TopStruct ;
cluster a_component  ->  connected for Element of K10( the carrier of GX);
coherence
 for b1 being Subset of GX st b1 is a_component holds
b1 is connected by Def5;
end;

registration
let GX be non empty TopSpace;
cluster a_component  ->  non empty for Element of K10( the carrier of GX);
coherence
 for b1 being Subset of GX st b1 is a_component holds
not b1 is empty
proof
 {} c= { the Point of GX} by XBOOLE_1:2;
hence  for b1 being Subset of GX st b1 is a_component holds
not b1 is empty by Def5; ::_thesis: verum
end;
end;

theorem :: CONNSP_1:32
for GX being non empty TopSpace
for A being Subset of GX st A is a_component holds
A <> {} GX ;

registration
let GX be TopSpace;
cluster a_component  ->  closed for Element of K10( the carrier of GX);
coherence
 for b1 being Subset of GX st b1 is a_component holds
b1 is closed
proof
let A be Subset of GX; ::_thesis: ( A is a_component implies A is closed )
A1: A c= Cl A by PRE_TOPC:18;
assume A2: A is a_component ; ::_thesis: A is closed
then  Cl A is connected by Th19;
then  A = Cl A by A2, A1, Def5;
hence  A is closed by PRE_TOPC:22; ::_thesis: verum
end;
end;

theorem :: CONNSP_1:33
for GX being TopSpace
for A being Subset of GX st A is a_component holds
A is closed ;

theorem Th34: :: CONNSP_1:34
for GX being TopSpace
for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds
A,B are_separated
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds
A,B are_separated
let A, B be Subset of GX; ::_thesis: ( A is a_component & B is a_component & not A = B implies A,B are_separated )
assume that
A1: A is a_component and
A2: B is a_component ; ::_thesis: ( A = B or A,B are_separated )
 ( A <> B implies A,B are_separated )
proof
A3: B c= A \/ B by XBOOLE_1:7;
A4: A c= A \/ B by XBOOLE_1:7;
assume A5: A <> B ; ::_thesis: A,B are_separated
assume  not A,B are_separated ; ::_thesis: contradiction
then  A \/ B is connected by A1, A2, Th17;
then  A = A \/ B by A1, A4, Def5;
hence  contradiction by A1, A2, A5, A3, Def5; ::_thesis: verum
end;
hence  ( A = B or A,B are_separated ) ; ::_thesis: verum
end;

theorem :: CONNSP_1:35
for GX being TopSpace
for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds
A misses B by Th1, Th34;

theorem :: CONNSP_1:36
for GX being TopSpace
for C being Subset of GX st C is connected holds
for S being Subset of GX holds
( not S is a_component or C misses S or C c= S )
proof
let GX be TopSpace; ::_thesis: for C being Subset of GX st C is connected holds
for S being Subset of GX holds
( not S is a_component or C misses S or C c= S )
let C be Subset of GX; ::_thesis: ( C is connected implies for S being Subset of GX holds
( not S is a_component or C misses S or C c= S ) )
assume A1: C is connected ; ::_thesis: for S being Subset of GX holds
( not S is a_component or C misses S or C c= S )
let S be Subset of GX; ::_thesis: ( not S is a_component or C misses S or C c= S )
assume A2: S is a_component ; ::_thesis: ( C misses S or C c= S )
A3: S c= C \/ S by XBOOLE_1:7;
assume  C meets S ; ::_thesis: C c= S
then  C \/ S is connected by A1, A2, Th1, Th17;
then  S = C \/ S by A2, A3, Def5;
hence  C c= S by XBOOLE_1:7; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let A, B be Subset of GX;
predB is_a_component_of A means :Def6: :: CONNSP_1:def 6
 ex B1 being Subset of (GX | A) st
( B1 = B & B1 is a_component );
end;

:: deftheorem Def6 defines is_a_component_of CONNSP_1:def_6_:_
 for GX being TopStruct
for A, B being Subset of GX holds
( B is_a_component_of A iff ex B1 being Subset of (GX | A) st
( B1 = B & B1 is a_component ) );

theorem :: CONNSP_1:37
for GX being TopSpace
for A, C being Subset of GX st GX is connected & A is connected & C is_a_component_of ([#] GX) \ A holds
([#] GX) \ C is connected
proof
let GX be TopSpace; ::_thesis: for A, C being Subset of GX st GX is connected & A is connected & C is_a_component_of ([#] GX) \ A holds
([#] GX) \ C is connected
let A, C be Subset of GX; ::_thesis: ( GX is connected & A is connected & C is_a_component_of ([#] GX) \ A implies ([#] GX) \ C is connected )
assume that
A1: GX is connected and
A2: A is connected and
A3: C is_a_component_of ([#] GX) \ A ; ::_thesis: ([#] GX) \ C is connected
consider C1 being Subset of (GX | (([#] GX) \ A)) such that
A4: C1 = C and
A5: C1 is a_component by A3, Def6;
reconsider C2 = C1 as Subset of GX by A4;
 C1 c= [#] (GX | (([#] GX) \ A)) ;
then  C1 c= ([#] GX) \ A by PRE_TOPC:def_5;
then  (([#] GX) \ A) ` c= C2 ` by SUBSET_1:12;
then A6: A c= C2 ` by PRE_TOPC:3;
now__::_thesis:_for_P,_Q_being_Subset_of_GX_st_([#]_GX)_\_C_=_P_\/_Q_&_P,Q_are_separated_&_not_P_=_{}_GX_holds_
Q_=_{}_GX
 A misses C1 by A6, SUBSET_1:23;
then A7: A /\ C1 = {} by XBOOLE_0:def_7;
A8: C is connected by A4, A5, Th23;
let P, Q be Subset of GX; ::_thesis: ( ([#] GX) \ C = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )
assume that
A9: ([#] GX) \ C = P \/ Q and
A10: P,Q are_separated ; ::_thesis: ( P = {} GX or Q = {} GX )
A11: P misses P ` by XBOOLE_1:79;
A12: P misses Q by A10, Th1;
A13: now__::_thesis:_(_A_c=_Q_implies_P_=_{}_GX_)
A14: Q misses Q ` by XBOOLE_1:79;
assume A15: A c= Q ; ::_thesis: P = {} GX
 P c= Q ` by A12, SUBSET_1:23;
then  A /\ P c= Q /\ (Q `) by A15, XBOOLE_1:27;
then A16: A /\ P c= {} by A14, XBOOLE_0:def_7;
(C \/ P) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by A4, A7, A16 ;
then  C \/ P misses A by XBOOLE_0:def_7;
then  C \/ P c= A ` by SUBSET_1:23;
then  C \/ P c= [#] (GX | (([#] GX) \ A)) by PRE_TOPC:def_5;
then reconsider C1P1 = C \/ P as Subset of (GX | (([#] GX) \ A)) ;
A17: C misses C ` by XBOOLE_1:79;
 C \/ P is connected by A1, A9, A10, A8, Th20;
then A18: C1P1 is connected by Th23;
 C c= C1 \/ P by A4, XBOOLE_1:7;
then  C1P1 = C1 by A4, A5, A18, Def5;
then A19: P c= C by A4, XBOOLE_1:7;
 P c= ([#] GX) \ C by A9, XBOOLE_1:7;
then  P c= C /\ (([#] GX) \ C) by A19, XBOOLE_1:19;
then  P c= {} by A17, XBOOLE_0:def_7;
hence  P = {} GX ; ::_thesis: verum
end;
A20: Q c= ([#] GX) \ C by A9, XBOOLE_1:7;
now__::_thesis:_(_A_c=_P_implies_Q_=_{}_GX_)
assume A21: A c= P ; ::_thesis: Q = {} GX
 Q c= P ` by A12, SUBSET_1:23;
then  A /\ Q c= P /\ (P `) by A21, XBOOLE_1:27;
then A22: A /\ Q c= {} by A11, XBOOLE_0:def_7;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by A4, A7, A22 ;
then  C \/ Q misses A by XBOOLE_0:def_7;
then  C \/ Q c= A ` by SUBSET_1:23;
then  C \/ Q c= [#] (GX | (([#] GX) \ A)) by PRE_TOPC:def_5;
then reconsider C1Q1 = C \/ Q as Subset of (GX | (([#] GX) \ A)) ;
 C \/ Q is connected by A1, A9, A10, A8, Th20;
then A23: C1Q1 is connected by Th23;
 C1 c= C1 \/ Q by XBOOLE_1:7;
then  C1Q1 = C1 by A4, A5, A23, Def5;
then  Q c= C by A4, XBOOLE_1:7;
then A24: Q c= C /\ (([#] GX) \ C) by A20, XBOOLE_1:19;
 C misses C ` by XBOOLE_1:79;
then  Q c= {} by A24, XBOOLE_0:def_7;
hence  Q = {} GX ; ::_thesis: verum
end;
hence  ( P = {} GX or Q = {} GX ) by A2, A4, A6, A9, A10, A13, Th16; ::_thesis: verum
end;
hence  ([#] GX) \ C is connected by Th15; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let x be Point of GX;
func Component_of x ->  Subset of GX means :Def7: :: CONNSP_1:def 7
 ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = it );
existence
 ex b1 being Subset of GX ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = b1 )
proof
defpred S1[ set ] means  ex A1 being Subset of GX st
( A1 = $1 & A1 is connected & x in $1 );
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
take  union F ; ::_thesis: ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = union F )
take  F ; ::_thesis: ( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = union F )
thus  for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ::_thesis: union F = union F
proof
let A be Subset of GX; ::_thesis: ( A in F iff ( A is connected & x in A ) )
thus  ( A in F implies ( A is connected & x in A ) ) ::_thesis: ( A is connected & x in A implies A in F )
proof
assume  A in F ; ::_thesis: ( A is connected & x in A )
then  ex A1 being Subset of GX st
( A1 = A & A1 is connected & x in A ) by A1;
hence  ( A is connected & x in A ) ; ::_thesis: verum
end;
thus  ( A is connected & x in A implies A in F ) by A1; ::_thesis: verum
end;
thus  union F = union F ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of GX st ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = b1 ) & ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = b2 ) holds
b1 = b2
proof
let S, S9 be Subset of GX; ::_thesis: ( ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S ) & ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S9 ) implies S = S9 )
assume that
A2: ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S ) and
A3: ex F9 being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F9 iff ( A is connected & x in A ) ) ) & union F9 = S9 ) ; ::_thesis: S = S9
consider F being Subset-Family of GX such that
A4: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A5: union F = S by A2;
consider F9 being Subset-Family of GX such that
A6: for A being Subset of GX holds
( A in F9 iff ( A is connected & x in A ) ) and
A7: union F9 = S9 by A3;
now__::_thesis:_for_y_being_set_holds_
(_y_in_S_iff_y_in_S9_)
let y be set ; ::_thesis: ( y in S iff y in S9 )
A8: now__::_thesis:_(_y_in_S9_implies_y_in_S_)
assume  y in S9 ; ::_thesis: y in S
then consider B being set  such that
A9: y in B and
A10: B in F9 by A7, TARSKI:def_4;
reconsider B = B as Subset of GX by A10;
A11: x in B by A6, A10;
 B is connected by A6, A10;
then  B in F by A4, A11;
hence  y in S by A5, A9, TARSKI:def_4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_S_implies_y_in_S9_)
assume  y in S ; ::_thesis: y in S9
then consider B being set  such that
A12: y in B and
A13: B in F by A5, TARSKI:def_4;
reconsider B = B as Subset of GX by A13;
A14: x in B by A4, A13;
 B is connected by A4, A13;
then  B in F9 by A6, A14;
hence  y in S9 by A7, A12, TARSKI:def_4; ::_thesis: verum
end;
hence  ( y in S iff y in S9 ) by A8; ::_thesis: verum
end;
hence  S = S9 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Component_of CONNSP_1:def_7_:_
 for GX being TopStruct
for x being Point of GX
for b3 being Subset of GX holds
( b3 = Component_of x iff ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = b3 ) );


theorem Th38: :: CONNSP_1:38
for GX being non empty TopSpace
for x being Point of GX holds x in Component_of x
proof
let GX be non empty TopSpace; ::_thesis: for x being Point of GX holds x in Component_of x
let x be Point of GX; ::_thesis: x in Component_of x
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A2: Component_of x = union F by Def7;
A3: for A being set st A in F holds
x in A by A1;
 F <> {} by A1, Th31;
then A4: x in meet F by A3, SETFAM_1:def_1;
 meet F c= union F by SETFAM_1:2;
hence  x in Component_of x by A2, A4; ::_thesis: verum
end;

registration
let GX be non empty TopSpace;
let x be Point of GX;
cluster Component_of x ->  non empty connected ;
coherence
 ( not Component_of x is empty & Component_of x is connected )
proof
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A2: Component_of x = union F by Def7;
A3: for A being set st A in F holds
x in A by A1;
 F <> {} by A1, Th31;
then A4: meet F <> {} GX by A3, SETFAM_1:def_1;
 for A being Subset of GX st A in F holds
A is connected by A1;
hence  ( not Component_of x is empty & Component_of x is connected ) by A2, A4, Th26, Th38; ::_thesis: verum
end;
end;

theorem Th39: :: CONNSP_1:39
for GX being non empty TopSpace
for C being Subset of GX
for x being Point of GX st C is connected & Component_of x c= C holds
C = Component_of x
proof
let GX be non empty TopSpace; ::_thesis: for C being Subset of GX
for x being Point of GX st C is connected & Component_of x c= C holds
C = Component_of x
let C be Subset of GX; ::_thesis: for x being Point of GX st C is connected & Component_of x c= C holds
C = Component_of x
let x be Point of GX; ::_thesis: ( C is connected & Component_of x c= C implies C = Component_of x )
assume A1: C is connected ; ::_thesis: ( not Component_of x c= C or C = Component_of x )
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A3: Component_of x = union F by Def7;
assume A4: Component_of x c= C ; ::_thesis: C = Component_of x
 x in Component_of x by Th38;
then  C in F by A1, A4, A2;
then  C c= Component_of x by A3, ZFMISC_1:74;
hence  C = Component_of x by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th40: :: CONNSP_1:40
for GX being non empty TopSpace
for A being Subset of GX holds
( A is a_component iff ex x being Point of GX st A = Component_of x )
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX holds
( A is a_component iff ex x being Point of GX st A = Component_of x )
let A be Subset of GX; ::_thesis: ( A is a_component iff ex x being Point of GX st A = Component_of x )
hereby  ::_thesis: ( ex x being Point of GX st A = Component_of x implies A is a_component )
assume A1: A is a_component ; ::_thesis: ex x being Point of GX st A = Component_of x
then  A <> {} GX ;
then consider y being Point of GX such that
A2: y in A by PRE_TOPC:12;
take x = y; ::_thesis: A = Component_of x
consider F being Subset-Family of GX such that
A3: for B being Subset of GX holds
( B in F iff ( B is connected & x in B ) ) and
A4: union F = Component_of x by Def7;
 A in F by A1, A2, A3;
then  A c= union F by ZFMISC_1:74;
hence  A = Component_of x by A1, A4, Def5; ::_thesis: verum
end;
given x being Point of GX such that A5: A = Component_of x ; ::_thesis: A is a_component
 for B being Subset of GX st B is connected & A c= B holds
A = B by A5, Th39;
hence  A is a_component by A5, Def5; ::_thesis: verum
end;

theorem :: CONNSP_1:41
for GX being non empty TopSpace
for A being Subset of GX
for x being Point of GX st A is a_component & x in A holds
A = Component_of x
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX
for x being Point of GX st A is a_component & x in A holds
A = Component_of x
let A be Subset of GX; ::_thesis: for x being Point of GX st A is a_component & x in A holds
A = Component_of x
let x be Point of GX; ::_thesis: ( A is a_component & x in A implies A = Component_of x )
assume that
A1: A is a_component and
A2: x in A ; ::_thesis: A = Component_of x
 x in Component_of x by Th38;
then  A /\ (Component_of x) <> {} by A2, XBOOLE_0:def_4;
then A3: A meets Component_of x by XBOOLE_0:def_7;
A4: Component_of x is a_component by Th40;
assume  A <> Component_of x ; ::_thesis: contradiction
hence  contradiction by A1, A3, A4, Th1, Th34; ::_thesis: verum
end;

theorem :: CONNSP_1:42
for GX being non empty TopSpace
for x, p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
proof
let GX be non empty TopSpace; ::_thesis: for x, p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
let x be Point of GX; ::_thesis: for p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
set A = Component_of x;
A1: Component_of x is a_component by Th40;
given p being Point of GX such that A2: p in Component_of x and
A3: Component_of p <> Component_of x ; ::_thesis: contradiction
 Component_of p is a_component by Th40;
then  Component_of p misses Component_of x by A3, A1, Th1, Th34;
then A4: (Component_of p) /\ (Component_of x) = {} GX by XBOOLE_0:def_7;
 p in Component_of p by Th38;
hence  contradiction by A2, A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: CONNSP_1:43
for GX being non empty TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff A is a_component ) ) holds
F is Cover of GX
proof
let GX be non empty TopSpace; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff A is a_component ) ) holds
F is Cover of GX
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX holds
( A in F iff A is a_component ) ) implies F is Cover of GX )
assume A1: for A being Subset of GX holds
( A in F iff A is a_component ) ; ::_thesis: F is Cover of GX
now__::_thesis:_for_x_being_set_st_x_in_[#]_GX_holds_
x_in_union_F
let x be set ; ::_thesis: ( x in [#] GX implies x in union F )
assume  x in [#] GX ; ::_thesis: x in union F
then reconsider y = x as Point of GX ;
 Component_of y is a_component by Th40;
then  Component_of y in F by A1;
then A2: Component_of y c= union F by ZFMISC_1:74;
 y in Component_of y by Th38;
hence  x in union F by A2; ::_thesis: verum
end;
then  [#] GX c= union F by TARSKI:def_3;
hence  F is Cover of GX by SETFAM_1:def_11; ::_thesis: verum
end;

begin

registration
let T be TopStruct ;
cluster empty for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st b1 is empty
proof
take  {} T ; ::_thesis: {} T is empty
thus  {} T is empty ; ::_thesis: verum
end;
end;

registration
let T be TopStruct ;
cluster empty  ->  connected for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is connected
proof
let C be Subset of T; ::_thesis: ( C is empty implies C is connected )
assume  C is empty ; ::_thesis: C is connected
then reconsider D = C as empty Subset of T ;
let A, B be Subset of (T | C); :: according to CONNSP_1:def_2,CONNSP_1:def_3 ::_thesis: ( [#] (T | C) = A \/ B & A,B are_separated & not A = {} (T | C) implies B = {} (T | C) )
assume that
 [#] (T | C) = A \/ B and
 A,B are_separated ; ::_thesis: ( A = {} (T | C) or B = {} (T | C) )
 [#] (T | D) = {} ;
hence  ( A = {} (T | C) or B = {} (T | C) ) ; ::_thesis: verum
end;
end;

theorem Th44: :: CONNSP_1:44
for T being TopSpace
for X being set holds
( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be TopSpace; ::_thesis: for X being set holds
( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )
thus  ( X is connected Subset of T implies X is connected Subset of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( X is connected Subset of TopStruct(# the carrier of T, the topology of T #) implies X is connected Subset of T )
proof
assume A1: X is connected Subset of T ; ::_thesis: X is connected Subset of TopStruct(# the carrier of T, the topology of T #)
then reconsider X = X as Subset of T ;
reconsider Y = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
 TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y by PRE_TOPC:36;
then  TopStruct(# the carrier of T, the topology of T #) | Y is connected by A1, Def3;
hence  X is connected Subset of TopStruct(# the carrier of T, the topology of T #) by Def3; ::_thesis: verum
end;
assume A2: X is connected Subset of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: X is connected Subset of T
then reconsider X = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
reconsider Y = X as Subset of T ;
 TopStruct(# the carrier of (T | Y), the topology of (T | Y) #) = TopStruct(# the carrier of T, the topology of T #) | X by PRE_TOPC:36;
then  T | Y is connected by A2, Def3;
hence  X is connected Subset of T by Def3; ::_thesis: verum
end;

theorem :: CONNSP_1:45
for T being TopSpace
for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
( X is a_component iff Y is a_component )
proof
let T be TopSpace; ::_thesis: for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
( X is a_component iff Y is a_component )
let X be Subset of T; ::_thesis: for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
( X is a_component iff Y is a_component )
let Y be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( X = Y implies ( X is a_component iff Y is a_component ) )
assume A1: X = Y ; ::_thesis: ( X is a_component iff Y is a_component )
thus  ( X is a_component implies Y is a_component ) ::_thesis: ( Y is a_component implies X is a_component )
proof
assume A2: X is a_component ; ::_thesis: Y is a_component
hence  Y is connected by A1, Th44; :: according to CONNSP_1:def_5 ::_thesis: for B being Subset of TopStruct(# the carrier of T, the topology of T #) st B is connected & Y c= B holds
Y = B
let B be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( B is connected & Y c= B implies Y = B )
assume that
A3: B is connected and
A4: Y c= B ; ::_thesis: Y = B
reconsider C = B as Subset of T ;
 C is connected by A3, Th44;
hence  Y = B by A1, A2, A4, Def5; ::_thesis: verum
end;
assume A5: Y is a_component ; ::_thesis: X is a_component
hence  X is connected by A1, Th44; :: according to CONNSP_1:def_5 ::_thesis: for B being Subset of T st B is connected & X c= B holds
X = B
let B be Subset of T; ::_thesis: ( B is connected & X c= B implies X = B )
assume that
A6: B is connected and
A7: X c= B ; ::_thesis: X = B
reconsider C = B as Subset of TopStruct(# the carrier of T, the topology of T #) ;
 C is connected by A6, Th44;
hence  X = B by A1, A5, A7, Def5; ::_thesis: verum
end;

theorem :: CONNSP_1:46
for G being non empty TopSpace
for P, A being Subset of G
for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
proof
let G be non empty TopSpace; ::_thesis: for P, A being Subset of G
for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
let P, A be Subset of G; ::_thesis: for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
let Q be Subset of (G | A); ::_thesis: ( P = Q & P is connected implies Q is connected )
assume that
A1: P = Q and
A2: P is connected ; ::_thesis: Q is connected
A3: G | P is connected by A2, Def3;
 Q c= the carrier of (G | A) ;
then  Q c= A by PRE_TOPC:8;
then  G | P = (G | A) | Q by A1, PRE_TOPC:7;
hence  Q is connected by A3, Def3; ::_thesis: verum
end;