:: CONNSP_3 semantic presentation

begin


definition
let GX be TopStruct ;
let V be Subset of GX;
func Component_of V ->  Subset of GX means :Def1: :: CONNSP_3:def 1
 ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & V c= 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 & V c= A ) ) ) & union F = b1 )
proof
defpred S1[ set ] means  ex A1 being Subset of GX st
( A1 = $1 & A1 is connected & V c= $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 & V c= A ) ) ) & union F = union F )
take  F ; ::_thesis: ( ( for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )
thus  for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) ::_thesis: union F = union F
proof
let A be Subset of GX; ::_thesis: ( A in F iff ( A is connected & V c= A ) )
thus  ( A in F implies ( A is connected & V c= A ) ) ::_thesis: ( A is connected & V c= A implies A in F )
proof
assume  A in F ; ::_thesis: ( A is connected & V c= A )
then  ex A1 being Subset of GX st
( A1 = A & A1 is connected & V c= A ) by A1;
hence  ( A is connected & V c= A ) ; ::_thesis: verum
end;
thus  ( A is connected & V c= 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 & V c= 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 & V c= 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 & V c= 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 & V c= 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 & V c= 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 & V c= 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 & V c= 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 & V c= 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;
 ( B is connected & V c= B ) by A6, A10;
then  B in F by A4;
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
A11: y in B and
A12: B in F by A5, TARSKI:def_4;
reconsider B = B as Subset of GX by A12;
 ( B is connected & V c= B ) by A4, A12;
then  B in F9 by A6;
hence  y in S9 by A7, A11, 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 Def1 defines Component_of CONNSP_3:def_1_:_
 for GX being TopStruct
for V, b3 being Subset of GX holds
( b3 = Component_of V iff ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = b3 ) );

theorem Th1: :: CONNSP_3:1
for GX being TopSpace
for V being Subset of GX st ex A being Subset of GX st
( A is connected & V c= A ) holds
V c= Component_of V
proof
let GX be TopSpace; ::_thesis: for V being Subset of GX st ex A being Subset of GX st
( A is connected & V c= A ) holds
V c= Component_of V
let V be Subset of GX; ::_thesis: ( ex A being Subset of GX st
( A is connected & V c= A ) implies V c= Component_of V )
given A being Subset of GX such that A1: ( A is connected & V c= A ) ; ::_thesis: V c= Component_of V
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A3: Component_of V = union F by Def1;
A4: for A being set st A in F holds
V c= A by A2;
 F <> {} by A1, A2;
then A5: V c= meet F by A4, SETFAM_1:5;
 meet F c= union F by SETFAM_1:2;
hence  V c= Component_of V by A3, A5, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: CONNSP_3:2
for GX being TopSpace
for V being Subset of GX st ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) holds
Component_of V = {}
proof
let GX be TopSpace; ::_thesis: for V being Subset of GX st ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) holds
Component_of V = {}
let V be Subset of GX; ::_thesis: ( ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) implies Component_of V = {} )
assume A1: for A being Subset of GX holds
( not A is connected or not V c= A ) ; ::_thesis: Component_of V = {}
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A3: Component_of V = union F by Def1;
now__::_thesis:_not_F_<>_{}
assume  F <> {} ; ::_thesis: contradiction
then consider A being Subset of GX such that
A4: A in F by SUBSET_1:4;
reconsider A = A as Subset of GX ;
 ( A is connected & V c= A ) by A2, A4;
hence  contradiction by A1; ::_thesis: verum
end;
hence  Component_of V = {} by A3, ZFMISC_1:2; ::_thesis: verum
end;

theorem Th3: :: CONNSP_3:3
for GX being non empty TopSpace holds Component_of ({} GX) = the carrier of GX
proof
let GX be non empty TopSpace; ::_thesis: Component_of ({} GX) = the carrier of GX
defpred S1[ set ] means  ex A1 being Subset of GX st
( A1 = $1 & A1 is connected & {} GX c= $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();
A2: for A being Subset of GX holds
( A in F iff ( A is connected & {} GX c= A ) )
proof
let A be Subset of GX; ::_thesis: ( A in F iff ( A is connected & {} GX c= A ) )
thus  ( A in F implies ( A is connected & {} GX c= A ) ) ::_thesis: ( A is connected & {} GX c= A implies A in F )
proof
assume  A in F ; ::_thesis: ( A is connected & {} GX c= A )
then  ex A1 being Subset of GX st
( A1 = A & A1 is connected & {} GX c= A ) by A1;
hence  ( A is connected & {} GX c= A ) ; ::_thesis: verum
end;
thus  ( A is connected & {} GX c= A implies A in F ) by A1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_GX_implies_ex_Y_being_set_st_
(_x_in_Y_&_Y_in_F_)_)_&_(_ex_Y_being_set_st_
(_x_in_Y_&_Y_in_F_)_implies_x_in_the_carrier_of_GX_)_)
let x be set ; ::_thesis: ( ( x in the carrier of GX implies ex Y being set st
( x in Y & Y in F ) ) & ( ex Y being set st
( x in Y & Y in F ) implies x in the carrier of GX ) )
hereby  ::_thesis: ( ex Y being set st
( x in Y & Y in F ) implies x in the carrier of GX )
assume  x in the carrier of GX ; ::_thesis: ex Y being set st
( x in Y & Y in F )
then reconsider p = x as Point of GX ;
reconsider Y = Component_of p as set ;
take Y = Y; ::_thesis: ( x in Y & Y in F )
thus  x in Y by CONNSP_1:38; ::_thesis: Y in F
 ( Component_of p is connected & {} GX c= Y ) by XBOOLE_1:2;
hence  Y in F by A2; ::_thesis: verum
end;
given Y being set  such that A3: ( x in Y & Y in F ) ; ::_thesis: x in the carrier of GX
thus  x in the carrier of GX by A3; ::_thesis: verum
end;
then  union F = the carrier of GX by TARSKI:def_4;
hence  Component_of ({} GX) = the carrier of GX by A2, Def1; ::_thesis: verum
end;

theorem :: CONNSP_3:4
for GX being non empty TopSpace
for V being Subset of GX st V is connected holds
Component_of V <> {}
proof
let GX be non empty TopSpace; ::_thesis: for V being Subset of GX st V is connected holds
Component_of V <> {}
let V be Subset of GX; ::_thesis: ( V is connected implies Component_of V <> {} )
assume A1: V is connected ; ::_thesis: Component_of V <> {}
percases ( V = {} or V <> {} ) ;
suppose V = {} ; ::_thesis: Component_of V <> {}
then  V = {} GX ;
hence  Component_of V <> {} by Th3; ::_thesis: verum
end;
suppose V <> {} ; ::_thesis: Component_of V <> {}
hence  Component_of V <> {} by A1, Th1, XBOOLE_1:3; ::_thesis: verum
end;
end;
end;

theorem Th5: :: CONNSP_3:5
for GX being TopSpace
for V being Subset of GX st V is connected & V <> {} holds
Component_of V is connected
proof
let GX be TopSpace; ::_thesis: for V being Subset of GX st V is connected & V <> {} holds
Component_of V is connected
let V be Subset of GX; ::_thesis: ( V is connected & V <> {} implies Component_of V is connected )
assume that
A1: V is connected and
A2: V <> {} ; ::_thesis: Component_of V is connected
consider F being Subset-Family of GX such that
A3: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A4: Component_of V = union F by Def1;
A5: for A being set st A in F holds
V c= A by A3;
 F <> {} by A1, A3;
then  V c= meet F by A5, SETFAM_1:5;
then A6: meet F <> {} GX by A2;
 for A being Subset of GX st A in F holds
A is connected by A3;
hence  Component_of V is connected by A4, A6, CONNSP_1:26; ::_thesis: verum
end;

theorem Th6: :: CONNSP_3:6
for GX being non empty TopSpace
for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds
C = Component_of V
proof
let GX be non empty TopSpace; ::_thesis: for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds
C = Component_of V
let V, C be Subset of GX; ::_thesis: ( V is connected & C is connected & Component_of V c= C implies C = Component_of V )
assume that
A1: V is connected and
A2: C is connected ; ::_thesis: ( not Component_of V c= C or C = Component_of V )
assume A3: Component_of V c= C ; ::_thesis: C = Component_of V
consider F being Subset-Family of GX such that
A4: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A5: Component_of V = union F by Def1;
 V c= Component_of V by A1, Th1;
then  V c= C by A3, XBOOLE_1:1;
then  C in F by A2, A4;
then  C c= Component_of V by A5, ZFMISC_1:74;
hence  C = Component_of V by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th7: :: CONNSP_3:7
for GX being non empty TopSpace
for A being Subset of GX st A is a_component holds
Component_of A = A
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A is a_component holds
Component_of A = A
let A be Subset of GX; ::_thesis: ( A is a_component implies Component_of A = A )
assume A1: A is a_component ; ::_thesis: Component_of A = A
then A2: A is connected ;
then A3: A c= Component_of A by Th1;
 A <> {} GX by A1;
then  Component_of A is connected by A2, Th5;
hence  Component_of A = A by A1, A3, CONNSP_1:def_5; ::_thesis: verum
end;

theorem Th8: :: CONNSP_3:8
for GX being non empty TopSpace
for A being Subset of GX holds
( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX holds
( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
let A be Subset of GX; ::_thesis: ( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
A1: now__::_thesis:_(_A_is_a_component_implies_ex_V_being_Subset_of_GX_st_
(_V_is_connected_&_V_<>_{}_&_A_=_Component_of_V_)_)
assume A2: A is a_component ; ::_thesis: ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V )
take V = A; ::_thesis: ( V is connected & V <> {} & A = Component_of V )
thus  ( V is connected & V <> {} & A = Component_of V ) by A2, Th7; ::_thesis: verum
end;
now__::_thesis:_(_ex_V_being_Subset_of_GX_st_
(_V_is_connected_&_V_<>_{}_&_A_=_Component_of_V_)_implies_A_is_a_component_)
given V being Subset of GX such that A3: ( V is connected & V <> {} & A = Component_of V ) ; ::_thesis: A is a_component
 ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) ) by A3, Th5, Th6;
hence  A is a_component by CONNSP_1:def_5; ::_thesis: verum
end;
hence  ( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) ) by A1; ::_thesis: verum
end;

theorem :: CONNSP_3:9
for GX being non empty TopSpace
for V being Subset of GX st V is connected & V <> {} holds
Component_of V is a_component by Th8;

theorem :: CONNSP_3:10
for GX being non empty TopSpace
for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds
A = Component_of V
proof
let GX be non empty TopSpace; ::_thesis: for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds
A = Component_of V
let A, V be Subset of GX; ::_thesis: ( A is a_component & V is connected & V c= A & V <> {} implies A = Component_of V )
assume that
A1: A is a_component and
A2: V is connected and
A3: V c= A and
A4: V <> {} ; ::_thesis: A = Component_of V
 V c= Component_of V by A2, Th1;
then A5: A meets Component_of V by A3, A4, XBOOLE_1:67;
assume A6: A <> Component_of V ; ::_thesis: contradiction
 Component_of V is a_component by A2, A4, Th8;
hence  contradiction by A1, A6, A5, CONNSP_1:1, CONNSP_1:34; ::_thesis: verum
end;

theorem Th11: :: CONNSP_3:11
for GX being non empty TopSpace
for V being Subset of GX st V is connected & V <> {} holds
Component_of (Component_of V) = Component_of V
proof
let GX be non empty TopSpace; ::_thesis: for V being Subset of GX st V is connected & V <> {} holds
Component_of (Component_of V) = Component_of V
let V be Subset of GX; ::_thesis: ( V is connected & V <> {} implies Component_of (Component_of V) = Component_of V )
assume  ( V is connected & V <> {} ) ; ::_thesis: Component_of (Component_of V) = Component_of V
then  Component_of V is a_component by Th8;
hence  Component_of (Component_of V) = Component_of V by Th7; ::_thesis: verum
end;

theorem Th12: :: CONNSP_3:12
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
Component_of A = Component_of B
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
Component_of A = Component_of B
let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A <> {} & A c= B implies Component_of A = Component_of B )
assume that
A1: A is connected and
A2: B is connected and
A3: A <> {} and
A4: A c= B ; ::_thesis: Component_of A = Component_of B
 B <> {} by A3, A4;
then A5: Component_of B is connected by A2, Th5;
A6: B c= Component_of B by A2, Th1;
then A7: A c= Component_of B by A4, XBOOLE_1:1;
A8: Component_of B c= Component_of A
proof
consider F being Subset-Family of GX such that
A9: for D being Subset of GX holds
( D in F iff ( D is connected & A c= D ) ) and
A10: union F = Component_of A by Def1;
 Component_of B in F by A7, A5, A9;
hence  Component_of B c= Component_of A by A10, ZFMISC_1:74; ::_thesis: verum
end;
A11: Component_of A is connected by A1, A3, Th5;
 Component_of A c= Component_of B
proof
consider F being Subset-Family of GX such that
A12: for D being Subset of GX holds
( D in F iff ( D is connected & B c= D ) ) and
A13: union F = Component_of B by Def1;
 B c= Component_of A by A6, A8, XBOOLE_1:1;
then  Component_of A in F by A11, A12;
hence  Component_of A c= Component_of B by A13, ZFMISC_1:74; ::_thesis: verum
end;
hence  Component_of A = Component_of B by A8, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th13: :: CONNSP_3:13
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
B c= Component_of A
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
B c= Component_of A
let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A <> {} & A c= B implies B c= Component_of A )
assume that
A1: A is connected and
A2: B is connected and
A3: ( A <> {} & A c= B ) ; ::_thesis: B c= Component_of A
 Component_of A = Component_of B by A1, A2, A3, Th12;
hence  B c= Component_of A by A2, Th1; ::_thesis: verum
end;

theorem Th14: :: CONNSP_3:14
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds
A \/ B c= Component_of A
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds
A \/ B c= Component_of A
let A, B be Subset of GX; ::_thesis: ( A is connected & A \/ B is connected & A <> {} implies A \/ B c= Component_of A )
assume that
A1: A is connected and
A2: A \/ B is connected and
A3: A <> {} ; ::_thesis: A \/ B c= Component_of A
 Component_of (A \/ B) = Component_of A by A1, A2, A3, Th12, XBOOLE_1:7;
hence  A \/ B c= Component_of A by A2, Th1; ::_thesis: verum
end;

theorem Th15: :: CONNSP_3:15
for GX being non empty TopSpace
for A being Subset of GX
for p being Point of GX st A is connected & p in A holds
Component_of p = Component_of A
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX
for p being Point of GX st A is connected & p in A holds
Component_of p = Component_of A
let A be Subset of GX; ::_thesis: for p being Point of GX st A is connected & p in A holds
Component_of p = Component_of A
let p be Point of GX; ::_thesis: ( A is connected & p in A implies Component_of p = Component_of A )
assume that
A1: A is connected and
A2: p in A ; ::_thesis: Component_of p = Component_of A
 ( A c= Component_of A & Component_of A is a_component ) by A1, A2, Th1, Th8;
hence  Component_of p = Component_of A by A2, CONNSP_1:41; ::_thesis: verum
end;

theorem :: CONNSP_3:16
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A meets B holds
( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A meets B holds
( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )
let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A meets B implies ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) )
A1: ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
A2: for C, D being Subset of GX st C is connected & D is connected & C /\ D <> {} holds
C \/ D c= Component_of C
proof
let C, D be Subset of GX; ::_thesis: ( C is connected & D is connected & C /\ D <> {} implies C \/ D c= Component_of C )
assume that
A3: C is connected and
A4: D is connected and
A5: C /\ D <> {} ; ::_thesis: C \/ D c= Component_of C
 C meets D by A5, XBOOLE_0:def_7;
then A6: C \/ D is connected by A3, A4, CONNSP_1:1, CONNSP_1:17;
 C <> {} by A5;
hence  C \/ D c= Component_of C by A3, A6, Th14; ::_thesis: verum
end;
assume  ( A is connected & B is connected & A /\ B <> {} ) ; :: according to XBOOLE_0:def_7 ::_thesis: ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )
then  ( A \/ B c= Component_of A & A \/ B c= Component_of B ) by A2;
hence  ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: CONNSP_3:17
for GX being non empty TopSpace
for A being Subset of GX st A is connected & A <> {} holds
Cl A c= Component_of A
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A is connected & A <> {} holds
Cl A c= Component_of A
let A be Subset of GX; ::_thesis: ( A is connected & A <> {} implies Cl A c= Component_of A )
assume that
A1: A is connected and
A2: A <> {} ; ::_thesis: Cl A c= Component_of A
 Cl A is connected by A1, CONNSP_1:19;
hence  Cl A c= Component_of A by A1, A2, Th13, PRE_TOPC:18; ::_thesis: verum
end;

theorem :: CONNSP_3:18
for GX being non empty TopSpace
for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds
A misses Component_of B
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds
A misses Component_of B
let A, B be Subset of GX; ::_thesis: ( A is a_component & B is connected & B <> {} & A misses B implies A misses Component_of B )
assume that
A1: A is a_component and
A2: ( B is connected & B <> {} ) and
A3: A /\ B = {} ; :: according to XBOOLE_0:def_7 ::_thesis: A misses Component_of B
A4: A is connected by A1;
assume  A /\ (Component_of B) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being Point of GX such that
A5: x in A /\ (Component_of B) by SUBSET_1:4;
 x in A by A5, XBOOLE_0:def_4;
then A6: Component_of x = Component_of A by A4, Th15;
A7: x in Component_of B by A5, XBOOLE_0:def_4;
 ( Component_of A = A & Component_of B = Component_of (Component_of B) ) by A1, A2, Th7, Th11;
then  (Component_of B) /\ B = {} by A2, A3, A7, A6, Th5, Th15;
hence  contradiction by A2, Th1, XBOOLE_1:28; ::_thesis: verum
end;

begin

Lm1: now__::_thesis:_for_GX_being_TopStruct_ex_F_being_Subset-Family_of_GX_st_
(_(_for_B_being_Subset_of_GX_st_B_in_F_holds_
B_is_a_component_)_&_{}_GX_=_union_F_)
let GX be TopStruct ; ::_thesis: ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & {} GX = union F )
reconsider S = {} as Subset-Family of GX by XBOOLE_1:2;
 for B being Subset of GX st B in S holds
B is a_component ;
hence  ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & {} GX = union F ) by ZFMISC_1:2; ::_thesis: verum
end;

definition
let GX be TopStruct ;
mode a_union_of_components of GX ->  Subset of GX means :Def2: :: CONNSP_3:def 2
 ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & it = union F );
existence
 ex b1 being Subset of GX ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & b1 = union F )
proof
take  {} GX ; ::_thesis: ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & {} GX = union F )
thus  ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & {} GX = union F ) by Lm1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines a_union_of_components CONNSP_3:def_2_:_
 for GX being TopStruct
for b2 being Subset of GX holds
( b2 is a_union_of_components of GX iff ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & b2 = union F ) );

theorem Th19: :: CONNSP_3:19
for GX being non empty TopSpace holds {} GX is a_union_of_components of GX
proof
let GX be non empty TopSpace; ::_thesis: {} GX is a_union_of_components of GX
thus  ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & {} GX = union F ) by Lm1; :: according to CONNSP_3:def_2 ::_thesis: verum
end;

theorem Th20: :: CONNSP_3:20
for GX being non empty TopSpace
for A being Subset of GX st A = the carrier of GX holds
A is a_union_of_components of GX
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A = the carrier of GX holds
A is a_union_of_components of GX
let A be Subset of GX; ::_thesis: ( A = the carrier of GX implies A is a_union_of_components of GX )
  {  B where B is Subset of GX : B is a_component  }  c= bool the carrier of GX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  B where B is Subset of GX : B is a_component  }  or x in bool the carrier of GX )
assume  x in  {  B where B is Subset of GX : B is a_component  }  ; ::_thesis: x in bool the carrier of GX
then  ex B being Subset of GX st
( x = B & B is a_component ) ;
hence  x in bool the carrier of GX ; ::_thesis: verum
end;
then reconsider S =  {  B where B is Subset of GX : B is a_component  }  as Subset-Family of GX ;
A1: for B being Subset of GX st B in S holds
B is a_component
proof
let B be Subset of GX; ::_thesis: ( B in S implies B is a_component )
assume  B in S ; ::_thesis: B is a_component
then  ex B2 being Subset of GX st
( B = B2 & B2 is a_component ) ;
hence  B is a_component ; ::_thesis: verum
end;
 the carrier of GX c= union S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of GX or x in union S )
assume  x in the carrier of GX ; ::_thesis: x in union S
then reconsider p = x as Point of GX ;
set B3 = Component_of p;
 Component_of p is a_component by CONNSP_1:40;
then  ( p in Component_of p & Component_of p in S ) by CONNSP_1:38;
hence  x in union S by TARSKI:def_4; ::_thesis: verum
end;
then A2: the carrier of GX = union S by XBOOLE_0:def_10;
assume  A = the carrier of GX ; ::_thesis: A is a_union_of_components of GX
hence  A is a_union_of_components of GX by A2, A1, Def2; ::_thesis: verum
end;

theorem Th21: :: CONNSP_3:21
for GX being non empty TopSpace
for A being Subset of GX
for p being Point of GX st p in A & A is a_union_of_components of GX holds
Component_of p c= A
proof
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX
for p being Point of GX st p in A & A is a_union_of_components of GX holds
Component_of p c= A
let A be Subset of GX; ::_thesis: for p being Point of GX st p in A & A is a_union_of_components of GX holds
Component_of p c= A
let p be Point of GX; ::_thesis: ( p in A & A is a_union_of_components of GX implies Component_of p c= A )
assume that
A1: p in A and
A2: A is a_union_of_components of GX ; ::_thesis: Component_of p c= A
consider F being Subset-Family of GX such that
A3: for B being Subset of GX st B in F holds
B is a_component and
A4: A = union F by A2, Def2;
consider X being set  such that
A5: p in X and
A6: X in F by A1, A4, TARSKI:def_4;
reconsider B2 = X as Subset of GX by A6;
 B2 = Component_of p by A3, A5, A6, CONNSP_1:41;
hence  Component_of p c= A by A4, A6, ZFMISC_1:74; ::_thesis: verum
end;

theorem :: CONNSP_3:22
for GX being non empty TopSpace
for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )
let A, B be Subset of GX; ::_thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) )
assume that
A1: A is a_union_of_components of GX and
A2: B is a_union_of_components of GX ; ::_thesis: ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )
consider Fa being Subset-Family of GX such that
A3: for Ba being Subset of GX st Ba in Fa holds
Ba is a_component and
A4: A = union Fa by A1, Def2;
consider Fb being Subset-Family of GX such that
A5: for Bb being Subset of GX st Bb in Fb holds
Bb is a_component and
A6: B = union Fb by A2, Def2;
A7: for B2 being Subset of GX st B2 in Fa \/ Fb holds
B2 is a_component
proof
let B2 be Subset of GX; ::_thesis: ( B2 in Fa \/ Fb implies B2 is a_component )
assume  B2 in Fa \/ Fb ; ::_thesis: B2 is a_component
then  ( B2 in Fa or B2 in Fb ) by XBOOLE_0:def_3;
hence  B2 is a_component by A3, A5; ::_thesis: verum
end;
A8: A /\ B is a_union_of_components of GX
proof
reconsider Fd = Fa /\ Fb as Subset-Family of GX ;
A9: for B4 being Subset of GX st B4 in Fd holds
B4 is a_component
proof
let B4 be Subset of GX; ::_thesis: ( B4 in Fd implies B4 is a_component )
assume  B4 in Fd ; ::_thesis: B4 is a_component
then  B4 in Fa by XBOOLE_0:def_4;
hence  B4 is a_component by A3; ::_thesis: verum
end;
A10: A /\ B c= union Fd
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ B or x in union Fd )
assume A11: x in A /\ B ; ::_thesis: x in union Fd
then  x in A by XBOOLE_0:def_4;
then consider F1 being set  such that
A12: x in F1 and
A13: F1 in Fa by A4, TARSKI:def_4;
reconsider C1 = F1 as Subset of GX by A13;
 x in B by A11, XBOOLE_0:def_4;
then consider F2 being set  such that
A14: x in F2 and
A15: F2 in Fb by A6, TARSKI:def_4;
reconsider C2 = F2 as Subset of GX by A15;
A16: C2 is a_component by A5, A15;
 C1 is a_component by A3, A13;
then A17: ( C1 = C2 or C1 misses C2 ) by A16, CONNSP_1:35;
 F1 /\ F2 <> {} by A12, A14, XBOOLE_0:def_4;
then  C1 in Fa /\ Fb by A13, A15, A17, XBOOLE_0:def_4, XBOOLE_0:def_7;
hence  x in union Fd by A12, TARSKI:def_4; ::_thesis: verum
end;
 union Fd c= A /\ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fd or x in A /\ B )
assume  x in union Fd ; ::_thesis: x in A /\ B
then consider X4 being set  such that
A18: x in X4 and
A19: X4 in Fd by TARSKI:def_4;
 X4 in Fb by A19, XBOOLE_0:def_4;
then A20: x in union Fb by A18, TARSKI:def_4;
 X4 in Fa by A19, XBOOLE_0:def_4;
then  x in union Fa by A18, TARSKI:def_4;
hence  x in A /\ B by A4, A6, A20, XBOOLE_0:def_4; ::_thesis: verum
end;
then  A /\ B = union Fd by A10, XBOOLE_0:def_10;
hence  A /\ B is a_union_of_components of GX by A9, Def2; ::_thesis: verum
end;
reconsider Fc = Fa \/ Fb as Subset-Family of GX ;
 A \/ B = union Fc by A4, A6, ZFMISC_1:78;
hence  ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) by A7, A8, Def2; ::_thesis: verum
end;

theorem :: CONNSP_3:23
for GX being non empty TopSpace
for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
union Fu is a_union_of_components of GX
proof
let GX be non empty TopSpace; ::_thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
union Fu is a_union_of_components of GX
let Fu be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) implies union Fu is a_union_of_components of GX )
  {  B where B is Subset of GX : ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component )  }  c= bool the carrier of GX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  B where B is Subset of GX : ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component )  }  or x in bool the carrier of GX )
assume  x in  {  B where B is Subset of GX : ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component )  }  ; ::_thesis: x in bool the carrier of GX
then  ex B being Subset of GX st
( x = B & ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component ) ) ;
hence  x in bool the carrier of GX ; ::_thesis: verum
end;
then reconsider F2 =  {  B where B is Subset of GX : ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component )  }  as Subset-Family of GX ;
A1: for B being Subset of GX st B in F2 holds
B is a_component
proof
let B be Subset of GX; ::_thesis: ( B in F2 implies B is a_component )
assume  B in F2 ; ::_thesis: B is a_component
then  ex A2 being Subset of GX st
( B = A2 & ex B2 being Subset of GX st
( B2 in Fu & A2 c= B2 & A2 is a_component ) ) ;
hence  B is a_component ; ::_thesis: verum
end;
assume A2: for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ; ::_thesis: union Fu is a_union_of_components of GX
A3: union Fu c= union F2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fu or x in union F2 )
assume  x in union Fu ; ::_thesis: x in union F2
then consider X2 being set  such that
A4: x in X2 and
A5: X2 in Fu by TARSKI:def_4;
reconsider B3 = X2 as Subset of GX by A5;
 B3 is a_union_of_components of GX by A2, A5;
then consider F being Subset-Family of GX such that
A6: for B being Subset of GX st B in F holds
B is a_component and
A7: B3 = union F by Def2;
consider Y2 being set  such that
A8: x in Y2 and
A9: Y2 in F by A4, A7, TARSKI:def_4;
reconsider A3 = Y2 as Subset of GX by A9;
 ( A3 is a_component & Y2 c= B3 ) by A6, A7, A9, ZFMISC_1:74;
then  A3 in F2 by A5;
hence  x in union F2 by A8, TARSKI:def_4; ::_thesis: verum
end;
 union F2 c= union Fu
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F2 or x in union Fu )
assume  x in union F2 ; ::_thesis: x in union Fu
then consider X being set  such that
A10: x in X and
A11: X in F2 by TARSKI:def_4;
 ex B being Subset of GX st
( X = B & ex B2 being Subset of GX st
( B2 in Fu & B c= B2 & B is a_component ) ) by A11;
hence  x in union Fu by A10, TARSKI:def_4; ::_thesis: verum
end;
then  union Fu = union F2 by A3, XBOOLE_0:def_10;
hence  union Fu is a_union_of_components of GX by A1, Def2; ::_thesis: verum
end;

theorem :: CONNSP_3:24
for GX being non empty TopSpace
for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
meet Fu is a_union_of_components of GX
proof
let GX be non empty TopSpace; ::_thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
meet Fu is a_union_of_components of GX
let Fu be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) implies meet Fu is a_union_of_components of GX )
assume A1: for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ; ::_thesis: meet Fu is a_union_of_components of GX
now__::_thesis:_(_(_Fu_<>_{}_&_meet_Fu_is_a_union_of_components_of_GX_)_or_(_Fu_=_{}_&_meet_Fu_is_a_union_of_components_of_GX_)_)
percases ( Fu <> {} or Fu = {} ) ;
caseA2: Fu <> {} ; ::_thesis: meet Fu is a_union_of_components of GX
  {  B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) )  }  c= bool the carrier of GX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) )  }  or x in bool the carrier of GX )
assume  x in  {  B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) )  }  ; ::_thesis: x in bool the carrier of GX
then  ex B being Subset of GX st
( x = B & B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) ;
hence  x in bool the carrier of GX ; ::_thesis: verum
end;
then reconsider F1 =  {  B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) )  }  as Subset-Family of GX ;
A3: meet Fu c= union F1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet Fu or x in union F1 )
consider Y2 being set  such that
A4: Y2 in Fu by A2, XBOOLE_0:def_1;
reconsider B2 = Y2 as Subset of GX by A4;
 B2 is a_union_of_components of GX by A1, A4;
then consider F being Subset-Family of GX such that
A5: for B being Subset of GX st B in F holds
B is a_component and
A6: B2 = union F by Def2;
assume A7: x in meet Fu ; ::_thesis: x in union F1
then  x in Y2 by A4, SETFAM_1:def_1;
then consider Y3 being set  such that
A8: x in Y3 and
A9: Y3 in F by A6, TARSKI:def_4;
reconsider B3 = Y3 as Subset of GX by A9;
A10: for A2 being Subset of GX st A2 in Fu holds
B3 c= A2
proof
reconsider p = x as Point of GX by A7;
let A2 be Subset of GX; ::_thesis: ( A2 in Fu implies B3 c= A2 )
assume A11: A2 in Fu ; ::_thesis: B3 c= A2
then  x in A2 by A7, SETFAM_1:def_1;
then  Component_of p c= A2 by A1, A11, Th21;
hence  B3 c= A2 by A5, A8, A9, CONNSP_1:41; ::_thesis: verum
end;
 B3 is a_component by A5, A9;
then  Y3 in F1 by A10;
hence  x in union F1 by A8, TARSKI:def_4; ::_thesis: verum
end;
A12: for B being Subset of GX st B in F1 holds
B is a_component
proof
let B be Subset of GX; ::_thesis: ( B in F1 implies B is a_component )
assume  B in F1 ; ::_thesis: B is a_component
then  ex B1 being Subset of GX st
( B = B1 & B1 is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B1 c= A2 ) ) ;
hence  B is a_component ; ::_thesis: verum
end;
 union F1 c= meet Fu
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F1 or x in meet Fu )
assume  x in union F1 ; ::_thesis: x in meet Fu
then consider X being set  such that
A13: x in X and
A14: X in F1 by TARSKI:def_4;
consider B being Subset of GX such that
A15: X = B and
 B is a_component and
A16: for A2 being Subset of GX st A2 in Fu holds
B c= A2 by A14;
 for Y being set st Y in Fu holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in Fu implies x in Y )
assume  Y in Fu ; ::_thesis: x in Y
then  B c= Y by A16;
hence  x in Y by A13, A15; ::_thesis: verum
end;
hence  x in meet Fu by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then  meet Fu = union F1 by A3, XBOOLE_0:def_10;
hence  meet Fu is a_union_of_components of GX by A12, Def2; ::_thesis: verum
end;
case Fu = {} ; ::_thesis: meet Fu is a_union_of_components of GX
then  meet Fu = {} GX by SETFAM_1:def_1;
hence  meet Fu is a_union_of_components of GX by Th19; ::_thesis: verum
end;
end;
end;
hence  meet Fu is a_union_of_components of GX ; ::_thesis: verum
end;

theorem :: CONNSP_3:25
for GX being non empty TopSpace
for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
A \ B is a_union_of_components of GX
proof
let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
A \ B is a_union_of_components of GX
let A, B be Subset of GX; ::_thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies A \ B is a_union_of_components of GX )
assume that
A1: A is a_union_of_components of GX and
A2: B is a_union_of_components of GX ; ::_thesis: A \ B is a_union_of_components of GX
consider Fa being Subset-Family of GX such that
A3: for B2 being Subset of GX st B2 in Fa holds
B2 is a_component and
A4: A = union Fa by A1, Def2;
consider Fb being Subset-Family of GX such that
A5: for B3 being Subset of GX st B3 in Fb holds
B3 is a_component and
A6: B = union Fb by A2, Def2;
reconsider Fd = Fa \ Fb as Subset-Family of GX ;
A7: union Fd c= A \ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fd or x in A \ B )
assume  x in union Fd ; ::_thesis: x in A \ B
then consider X being set  such that
A8: x in X and
A9: X in Fd by TARSKI:def_4;
reconsider A2 = X as Subset of GX by A9;
A10: not X in Fb by A9, XBOOLE_0:def_5;
A11: X in Fa by A9, XBOOLE_0:def_5;
then A12: A2 is a_component by A3;
A13: now__::_thesis:_not_x_in_B
assume  x in B ; ::_thesis: contradiction
then consider Y3 being set  such that
A14: x in Y3 and
A15: Y3 in Fb by A6, TARSKI:def_4;
reconsider B3 = Y3 as Subset of GX by A15;
 A2 /\ B3 <> {} by A8, A14, XBOOLE_0:def_4;
then A16: A2 meets B3 by XBOOLE_0:def_7;
 B3 is a_component by A5, A15;
hence  contradiction by A10, A12, A15, A16, CONNSP_1:35; ::_thesis: verum
end;
 A2 c= A by A4, A11, ZFMISC_1:74;
hence  x in A \ B by A8, A13, XBOOLE_0:def_5; ::_thesis: verum
end;
A17: for B4 being Subset of GX st B4 in Fd holds
B4 is a_component
proof
let B4 be Subset of GX; ::_thesis: ( B4 in Fd implies B4 is a_component )
assume  B4 in Fd ; ::_thesis: B4 is a_component
then  B4 in Fa by XBOOLE_0:def_5;
hence  B4 is a_component by A3; ::_thesis: verum
end;
 A \ B c= union Fd
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ B or x in union Fd )
assume A18: x in A \ B ; ::_thesis: x in union Fd
then  x in A by XBOOLE_0:def_5;
then consider X being set  such that
A19: x in X and
A20: X in Fa by A4, TARSKI:def_4;
reconsider A2 = X as Subset of GX by A20;
now__::_thesis:_not_A2_in_Fb
assume  A2 in Fb ; ::_thesis: contradiction
then  A2 c= B by A6, ZFMISC_1:74;
hence  contradiction by A18, A19, XBOOLE_0:def_5; ::_thesis: verum
end;
then  A2 in Fd by A20, XBOOLE_0:def_5;
hence  x in union Fd by A19, TARSKI:def_4; ::_thesis: verum
end;
then  A \ B = union Fd by A7, XBOOLE_0:def_10;
hence  A \ B is a_union_of_components of GX by A17, Def2; ::_thesis: verum
end;

begin

definition
let GX be TopStruct ;
let B be Subset of GX;
let p be Point of GX;
assume A1: p in B ;
func Down (p,B) ->  Point of (GX | B) equals :Def3: :: CONNSP_3:def 3
p;
coherence
 p is Point of (GX | B)
proof
 B = [#] (GX | B) by PRE_TOPC:def_5;
hence  p is Point of (GX | B) by A1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Down CONNSP_3:def_3_:_
 for GX being TopStruct
for B being Subset of GX
for p being Point of GX st p in B holds
Down (p,B) = p;

definition
let GX be TopStruct ;
let B be Subset of GX;
let p be Point of (GX | B);
assume A1: B <> {} ;
func Up p ->  Point of GX equals :: CONNSP_3:def 4
p;
coherence
 p is Point of GX
proof
 B = the carrier of (GX | B) by PRE_TOPC:8;
then  p in B by A1;
hence  p is Point of GX ; ::_thesis: verum
end;
end;

:: deftheorem  defines Up CONNSP_3:def_4_:_
 for GX being TopStruct
for B being Subset of GX
for p being Point of (GX | B) st B <> {} holds
Up p = p;

definition
let GX be TopStruct ;
let V, B be Subset of GX;
func Down (V,B) ->  Subset of (GX | B) equals :: CONNSP_3:def 5
V /\ B;
coherence
 V /\ B is Subset of (GX | B)
proof
 B = [#] (GX | B) by PRE_TOPC:def_5;
hence  V /\ B is Subset of (GX | B) by XBOOLE_1:17; ::_thesis: verum
end;
end;

:: deftheorem  defines Down CONNSP_3:def_5_:_
 for GX being TopStruct
for V, B being Subset of GX holds Down (V,B) = V /\ B;

definition
let GX be TopStruct ;
let B be Subset of GX;
let V be Subset of (GX | B);
func Up V ->  Subset of GX equals :: CONNSP_3:def 6
V;
coherence
 V is Subset of GX
proof
 B = the carrier of (GX | B) by PRE_TOPC:8;
hence  V is Subset of GX by XBOOLE_1:1; ::_thesis: verum
end;
end;

:: deftheorem  defines Up CONNSP_3:def_6_:_
 for GX being TopStruct
for B being Subset of GX
for V being Subset of (GX | B) holds Up V = V;

definition
let GX be TopStruct ;
let B be Subset of GX;
let p be Point of GX;
assume A1: p in B ;
func Component_of (p,B) ->  Subset of GX means :Def7: :: CONNSP_3:def 7
 for q being Point of (GX | B) st q = p holds
it = Component_of q;
existence
 ex b1 being Subset of GX st
for q being Point of (GX | B) st q = p holds
b1 = Component_of q
proof
A2: B = [#] (GX | B) by PRE_TOPC:def_5;
then reconsider q3 = p as Point of (GX | B) by A1;
reconsider C = Component_of q3 as Subset of GX by A2, XBOOLE_1:1;
take  C ; ::_thesis: for q being Point of (GX | B) st q = p holds
C = Component_of q
thus  for q being Point of (GX | B) st q = p holds
C = Component_of q ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of GX st ( for q being Point of (GX | B) st q = p holds
b1 = Component_of q ) & ( for q being Point of (GX | B) st q = p holds
b2 = Component_of q ) holds
b1 = b2
proof
 B = [#] (GX | B) by PRE_TOPC:def_5;
then reconsider q3 = p as Point of (GX | B) by A1;
let S, S9 be Subset of GX; ::_thesis: ( ( for q being Point of (GX | B) st q = p holds
S = Component_of q ) & ( for q being Point of (GX | B) st q = p holds
S9 = Component_of q ) implies S = S9 )
assume that
A3: for q being Point of (GX | B) st q = p holds
S = Component_of q and
A4: for q2 being Point of (GX | B) st q2 = p holds
S9 = Component_of q2 ; ::_thesis: S = S9
 S = Component_of q3 by A3;
hence  S = S9 by A4; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Component_of CONNSP_3:def_7_:_
 for GX being TopStruct
for B being Subset of GX
for p being Point of GX st p in B holds
for b4 being Subset of GX holds
( b4 = Component_of (p,B) iff for q being Point of (GX | B) st q = p holds
b4 = Component_of q );

theorem :: CONNSP_3:26
for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
p in Component_of (p,B)
proof
let GX be non empty TopSpace; ::_thesis: for B being Subset of GX
for p being Point of GX st p in B holds
p in Component_of (p,B)
let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds
p in Component_of (p,B)
let p be Point of GX; ::_thesis: ( p in B implies p in Component_of (p,B) )
assume A1: p in B ; ::_thesis: p in Component_of (p,B)
then reconsider B9 = B as non empty Subset of GX ;
reconsider q = p as Point of (GX | B9) by A1, PRE_TOPC:8;
 q in Component_of q by CONNSP_1:38;
hence  p in Component_of (p,B) by A1, Def7; ::_thesis: verum
end;

theorem Th27: :: CONNSP_3:27
for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
Component_of (p,B) = Component_of (Down (p,B))
proof
let GX be non empty TopSpace; ::_thesis: for B being Subset of GX
for p being Point of GX st p in B holds
Component_of (p,B) = Component_of (Down (p,B))
let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds
Component_of (p,B) = Component_of (Down (p,B))
let p be Point of GX; ::_thesis: ( p in B implies Component_of (p,B) = Component_of (Down (p,B)) )
assume A1: p in B ; ::_thesis: Component_of (p,B) = Component_of (Down (p,B))
then  p = Down (p,B) by Def3;
hence  Component_of (p,B) = Component_of (Down (p,B)) by A1, Def7; ::_thesis: verum
end;

theorem :: CONNSP_3:28
for GX being TopSpace
for V, B being Subset of GX st V is open holds
Down (V,B) is open
proof
let GX be TopSpace; ::_thesis: for V, B being Subset of GX st V is open holds
Down (V,B) is open
let V, B be Subset of GX; ::_thesis: ( V is open implies Down (V,B) is open )
assume  V is open ; ::_thesis: Down (V,B) is open
then A1: V in the topology of GX by PRE_TOPC:def_2;
 Down (V,B) = V /\ ([#] (GX | B)) by PRE_TOPC:def_5;
then  Down (V,B) in the topology of (GX | B) by A1, PRE_TOPC:def_4;
hence  Down (V,B) is open by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem Th29: :: CONNSP_3:29
for GX being non empty TopSpace
for V, B being Subset of GX st V c= B holds
Cl (Down (V,B)) = (Cl V) /\ B
proof
let GX be non empty TopSpace; ::_thesis: for V, B being Subset of GX st V c= B holds
Cl (Down (V,B)) = (Cl V) /\ B
let V, B be Subset of GX; ::_thesis: ( V c= B implies Cl (Down (V,B)) = (Cl V) /\ B )
assume  V c= B ; ::_thesis: Cl (Down (V,B)) = (Cl V) /\ B
then  Down (V,B) = V by XBOOLE_1:28;
then  Cl (Down (V,B)) = (Cl V) /\ ([#] (GX | B)) by PRE_TOPC:17;
hence  Cl (Down (V,B)) = (Cl V) /\ B by PRE_TOPC:def_5; ::_thesis: verum
end;

theorem :: CONNSP_3:30
for GX being non empty TopSpace
for B being Subset of GX
for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B
proof
let GX be non empty TopSpace; ::_thesis: for B being Subset of GX
for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B
let B be Subset of GX; ::_thesis: for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B
let V be Subset of (GX | B); ::_thesis: Cl V = (Cl (Up V)) /\ B
A1: B = [#] (GX | B) by PRE_TOPC:def_5;
then  Cl (Down ((Up V),B)) = (Cl (Up V)) /\ B by Th29;
hence  Cl V = (Cl (Up V)) /\ B by A1, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: CONNSP_3:31
for GX being non empty TopSpace
for V, B being Subset of GX st V c= B holds
Cl (Down (V,B)) c= Cl V
proof
let GX be non empty TopSpace; ::_thesis: for V, B being Subset of GX st V c= B holds
Cl (Down (V,B)) c= Cl V
let V, B be Subset of GX; ::_thesis: ( V c= B implies Cl (Down (V,B)) c= Cl V )
assume  V c= B ; ::_thesis: Cl (Down (V,B)) c= Cl V
then  Cl (Down (V,B)) = (Cl V) /\ B by Th29;
hence  Cl (Down (V,B)) c= Cl V by XBOOLE_1:17; ::_thesis: verum
end;

theorem :: CONNSP_3:32
for GX being non empty TopSpace
for B being Subset of GX
for V being Subset of (GX | B) st V c= B holds
Down ((Up V),B) = V by XBOOLE_1:28;

theorem :: CONNSP_3:33
for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
Component_of (p,B) is connected
proof
let GX be non empty TopSpace; ::_thesis: for B being Subset of GX
for p being Point of GX st p in B holds
Component_of (p,B) is connected
let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds
Component_of (p,B) is connected
let p be Point of GX; ::_thesis: ( p in B implies Component_of (p,B) is connected )
assume A1: p in B ; ::_thesis: Component_of (p,B) is connected
then reconsider B9 = B as non empty Subset of GX ;
 ( Component_of (Down (p,B9)) is connected & Component_of (p,B) = Component_of (Down (p,B)) ) by A1, Th27;
hence  Component_of (p,B) is connected by CONNSP_1:23; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster non empty for a_union_of_components of T;
existence
 not for b1 being a_union_of_components of T holds b1 is empty
proof
reconsider A = [#] T as a_union_of_components of T by Th20;
 not A is empty ;
hence  not for b1 being a_union_of_components of T holds b1 is empty ; ::_thesis: verum
end;
end;

theorem :: CONNSP_3:34
for T being non empty TopSpace
for A being non empty a_union_of_components of T st A is connected holds
A is a_component
proof
let T be non empty TopSpace; ::_thesis: for A being non empty a_union_of_components of T st A is connected holds
A is a_component
let A be non empty a_union_of_components of T; ::_thesis: ( A is connected implies A is a_component )
consider F being Subset-Family of T such that
A1: for B being Subset of T st B in F holds
B is a_component and
A2: A = union F by Def2;
consider X being set  such that
 X <> {} and
A3: X in F by A2, ORDERS_1:6;
reconsider X = X as Subset of T by A3;
assume A4: A is connected ; ::_thesis: A is a_component
 F = {X}
proof
thus  F c= {X} :: according to XBOOLE_0:def_10 ::_thesis: {X} c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in {X} )
assume A5: x in F ; ::_thesis: x in {X}
then reconsider Y = x as Subset of T ;
A6: ( X is a_component & X c= A ) by A1, A2, A3, ZFMISC_1:74;
 ( Y is a_component & Y c= A ) by A1, A2, A5, ZFMISC_1:74;
then Y = A by A4, CONNSP_1:def_5
.= X by A4, A6, CONNSP_1:def_5 ;
hence  x in {X} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in F )
assume  x in {X} ; ::_thesis: x in F
hence  x in F by A3, TARSKI:def_1; ::_thesis: verum
end;
then  A = X by A2, ZFMISC_1:25;
hence  A is a_component by A1, A3; ::_thesis: verum
end;