:: CONNSP_3 semantic presentation

begin

definition
let GX be ( ( ) ( ) TopStruct ) ;
let V be ( ( ) ( ) Subset of ) ;
func Component_of V -> ( ( ) ( ) Subset of ) means :: CONNSP_3:def 1
 ex F being ( ( ) ( ) Subset-Family of ) st
( ( for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Subset-Family of ) iff ( A : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Element of K10(K10(GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ) ) ) ) & union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of GX : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = it : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) );
end;

theorem :: CONNSP_3:1
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st ex A being ( ( ) ( ) Subset of ) st
( A : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) ) holds
V : ( ( ) ( ) Subset of ) c= Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:2
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st ( for A being ( ( ) ( ) Subset of ) holds
( not A : ( ( ) ( ) Subset of ) is connected or not V : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) ) ) holds
Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = {} : ( ( ) ( ) set ) ;

theorem :: CONNSP_3:3
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds Component_of ({} GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( empty closed connected ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) = the carrier of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ;

theorem :: CONNSP_3:4
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is connected holds
Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) ;

theorem :: CONNSP_3:5
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) is connected ;

theorem :: CONNSP_3:6
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V, C being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is connected & C : ( ( ) ( ) Subset of ) is connected & Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) c= C : ( ( ) ( ) Subset of ) holds
C : ( ( ) ( ) Subset of ) = Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:7
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is a_component holds
Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = A : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:8
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is a_component iff ex V being ( ( ) ( ) Subset of ) st
( V : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) & A : ( ( ) ( ) Subset of ) = Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ) ;

theorem :: CONNSP_3:9
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) is a_component ;

theorem :: CONNSP_3:10
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, V being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is a_component & V : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ) = Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:11
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is connected & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
Component_of (Component_of V : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = Component_of V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:12
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & B : ( ( ) ( ) Subset of ) is connected & A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) & A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = Component_of B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:13
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & B : ( ( ) ( ) Subset of ) is connected & A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) & A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
B : ( ( ) ( ) Subset of ) c= Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:14
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is connected & A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:15
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ) is connected & p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
Component_of p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty connected ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:16
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & B : ( ( ) ( ) Subset of ) is connected & A : ( ( ) ( ) Subset of ) meets B : ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Component_of B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= Component_of B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) c= Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ) ;

theorem :: CONNSP_3:17
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected & A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Component_of A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:18
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is a_component & B : ( ( ) ( ) Subset of ) is connected & B : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) & A : ( ( ) ( ) Subset of ) misses B : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) misses Component_of B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

begin

definition
let GX be ( ( ) ( ) TopStruct ) ;
mode a_union_of_components of GX -> ( ( ) ( ) Subset of ) means :: CONNSP_3:def 2
 ex F being ( ( ) ( ) Subset-Family of ) st
( ( for B being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Subset-Family of ) holds
B : ( ( ) ( ) Subset of ) is a_component ) & it : ( ( ) ( ) Element of K10(K10(GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of GX : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) );
end;

theorem :: CONNSP_3:19
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds {} GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( empty closed connected ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: CONNSP_3:20
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) holds
A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: CONNSP_3:21
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
Component_of p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty connected ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:22
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & B : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
( A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) ;

theorem :: CONNSP_3:23
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Fu being ( ( ) ( ) Subset-Family of ) st ( for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in Fu : ( ( ) ( ) Subset-Family of ) holds
A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) holds
union Fu : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: CONNSP_3:24
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Fu being ( ( ) ( ) Subset-Family of ) st ( for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in Fu : ( ( ) ( ) Subset-Family of ) holds
A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) holds
meet Fu : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: CONNSP_3:25
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & B : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
A : ( ( ) ( ) Subset of ) \ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_union_of_components of GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

begin

definition
let GX be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
let p be ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;
assume p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in B : ( ( ) ( ) Subset of ) ;
func Down (p,B) -> ( ( ) ( ) Point of ( ( ) ( ) set ) ) equals :: CONNSP_3:def 3
p : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) ;
end;

definition
let GX be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
let p be ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;
assume B : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( ) set ) ;
func Up p -> ( ( ) ( ) Point of ( ( ) ( ) set ) ) equals :: CONNSP_3:def 4
p : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) ;
end;

definition
let GX be ( ( ) ( ) TopStruct ) ;
let V, B be ( ( ) ( ) Subset of ) ;
func Down (V,B) -> ( ( ) ( ) Subset of ) equals :: CONNSP_3:def 5
V : ( ( ) ( ) Element of K10(K10(GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) Element of K10( the carrier of GX : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let GX be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
let V be ( ( ) ( ) Subset of ) ;
func Up V -> ( ( ) ( ) Subset of ) equals :: CONNSP_3:def 6
V : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) ;
end;

definition
let GX be ( ( ) ( ) TopStruct ) ;
let B be ( ( ) ( ) Subset of ) ;
let p be ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;
assume p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in B : ( ( ) ( ) Subset of ) ;
func Component_of (p,B) -> ( ( ) ( ) Subset of ) means :: CONNSP_3:def 7
 for q being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = p : ( ( ) ( ) Element of GX : ( ( ) ( ) TopStruct ) ) holds
it : ( ( ) ( ) set ) = Component_of q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K10( the carrier of (GX : ( ( ) ( ) TopStruct ) | B : ( ( ) ( ) Element of K10(K10(GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict ) SubSpace of GX : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: CONNSP_3:26
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) holds
p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Component_of (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) ;

theorem :: CONNSP_3:27
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) holds
Component_of (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) = Component_of (Down (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Subset of ) )) : ( ( ) ( ) Point of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K10( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CONNSP_3:28
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for V, B being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is open holds
Down (V : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) is open ;

theorem :: CONNSP_3:29
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V, B being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Cl (Down (V : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) )) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = (Cl V : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CONNSP_3:30
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of )
for V being ( ( ) ( ) Subset of ) holds Cl V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = (Cl (Up V : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CONNSP_3:31
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V, B being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Cl (Down (V : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) )) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= Cl V : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

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

theorem :: CONNSP_3:33
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) holds
Component_of (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) is connected ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster non empty for ( ( ) ( ) a_union_of_components of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ;
end;

theorem :: CONNSP_3:34
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( non empty ) ( non empty ) a_union_of_components of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st A : ( ( non empty ) ( non empty ) a_union_of_components of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is connected holds
A : ( ( non empty ) ( non empty ) a_union_of_components of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is a_component ;