:: COMPTS_1 semantic presentation

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
attr T is compact means :: COMPTS_1:def 1
 for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open holds
ex G being ( ( ) ( ) Subset-Family of ) st
( G : ( ( ) ( ) Subset-Family of ) c= F : ( ( ) ( ) Subset-Family of ) & G : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & G : ( ( ) ( ) Subset-Family of ) is finite );
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
redefine attr T is regular means :: COMPTS_1:def 2
 for p being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty finite V28() ) set ) & P : ( ( ) ( ) Subset of ) is closed & p : ( ( ) ( ) Subset of ) in P : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
ex W, V being ( ( ) ( ) Subset of ) st
( W : ( ( ) ( ) Subset of ) is open & V : ( ( ) ( ) Subset of ) is open & p : ( ( ) ( ) Subset of ) in W : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) c= V : ( ( ) ( ) Subset of ) & W : ( ( ) ( ) Subset of ) misses V : ( ( ) ( ) Subset of ) );
redefine attr T is normal means :: COMPTS_1:def 3
 for W, V being ( ( ) ( ) Subset of ) st W : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty finite V28() ) set ) & V : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty finite V28() ) set ) & W : ( ( ) ( ) Subset of ) is closed & V : ( ( ) ( ) Subset of ) is closed & W : ( ( ) ( ) Subset of ) misses V : ( ( ) ( ) Subset of ) holds
ex P, Q being ( ( ) ( ) Subset of ) st
( P : ( ( ) ( ) Subset of ) is open & Q : ( ( ) ( ) Subset of ) is open & W : ( ( ) ( ) Subset of ) c= P : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) c= Q : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) misses Q : ( ( ) ( ) Subset of ) );
end;

notation
let T be ( ( ) ( ) TopStruct ) ;
synonym Hausdorff T for T_2 ;
end;

definition
let T be ( ( ) ( ) TopStruct ) ;
let P be ( ( ) ( ) Subset of ) ;
attr P is compact means :: COMPTS_1:def 4
 for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of P : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & F : ( ( ) ( ) Subset-Family of ) is open holds
ex G being ( ( ) ( ) Subset-Family of ) st
( G : ( ( ) ( ) Subset-Family of ) c= F : ( ( ) ( ) Subset-Family of ) & G : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of P : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & G : ( ( ) ( ) Subset-Family of ) is finite );
end;

registration
let T be ( ( ) ( ) TopStruct ) ;
cluster empty -> compact for ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: COMPTS_1:1
for T being ( ( ) ( ) TopStruct ) holds
( T : ( ( ) ( ) TopStruct ) is compact iff [#] T : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is compact ) ;

theorem :: COMPTS_1:2
for T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) )
for Q being ( ( ) ( ) Subset of ) st Q : ( ( ) ( ) Subset of ) c= [#] A : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( Q : ( ( ) ( ) Subset of ) is compact iff for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = Q : ( ( ) ( ) Subset of ) holds
P : ( ( ) ( ) Subset of ) is compact ) ;

theorem :: COMPTS_1:3
for T being ( ( ) ( ) TopStruct )
for P being ( ( ) ( ) Subset of ) holds
( ( P : ( ( ) ( ) Subset of ) = {} : ( ( ) ( empty finite V28() ) set ) implies ( P : ( ( ) ( ) Subset of ) is compact iff T : ( ( ) ( ) TopStruct ) | P : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) is compact ) ) & ( T : ( ( ) ( ) TopStruct ) is TopSpace-like & P : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty finite V28() ) set ) implies ( P : ( ( ) ( ) Subset of ) is compact iff T : ( ( ) ( ) TopStruct ) | P : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) is compact ) ) ) ;

theorem :: COMPTS_1:4
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact iff for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is centered & F : ( ( ) ( ) Subset-Family of ) is closed holds
meet F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty finite V28() ) set ) ) ;

theorem :: COMPTS_1:5
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact iff for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty finite V28() ) set ) & F : ( ( ) ( ) Subset-Family of ) is closed & meet F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty finite V28() ) set ) holds
ex G being ( ( ) ( ) Subset-Family of ) st
( G : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty finite V28() ) set ) & G : ( ( ) ( ) Subset-Family of ) c= F : ( ( ) ( ) Subset-Family of ) & G : ( ( ) ( ) Subset-Family of ) is finite & meet G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty finite V28() ) set ) ) ) ;

theorem :: COMPTS_1:6
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is T_2 holds
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty finite V28() ) set ) & A : ( ( ) ( ) Subset of ) is compact holds
for p being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
ex PS, QS being ( ( ) ( ) Subset of ) st
( PS : ( ( ) ( ) Subset of ) is open & QS : ( ( ) ( ) Subset of ) is open & p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in PS : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= QS : ( ( ) ( ) Subset of ) & PS : ( ( ) ( ) Subset of ) misses QS : ( ( ) ( ) Subset of ) ) ;

theorem :: COMPTS_1:7
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for PS being ( ( ) ( ) Subset of ) st TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is T_2 & PS : ( ( ) ( ) Subset of ) is compact holds
PS : ( ( ) ( ) Subset of ) is closed ;

theorem :: COMPTS_1:8
for T being ( ( ) ( ) TopStruct )
for P being ( ( ) ( ) Subset of ) st T : ( ( ) ( ) TopStruct ) is compact & P : ( ( ) ( ) Subset of ) is closed holds
P : ( ( ) ( ) Subset of ) is compact ;

theorem :: COMPTS_1:9
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for PS, QS being ( ( ) ( ) Subset of ) st PS : ( ( ) ( ) Subset of ) is compact & QS : ( ( ) ( ) Subset of ) c= PS : ( ( ) ( ) Subset of ) & QS : ( ( ) ( ) Subset of ) is closed holds
QS : ( ( ) ( ) Subset of ) is compact ;

theorem :: COMPTS_1:10
for T being ( ( ) ( ) TopStruct )
for P, Q being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) is compact & Q : ( ( ) ( ) Subset of ) is compact holds
P : ( ( ) ( ) Subset of ) \/ Q : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is compact ;

theorem :: COMPTS_1:11
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for PS, QS being ( ( ) ( ) Subset of ) st TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is T_2 & PS : ( ( ) ( ) Subset of ) is compact & QS : ( ( ) ( ) Subset of ) is compact holds
PS : ( ( ) ( ) Subset of ) /\ QS : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is compact ;

theorem :: COMPTS_1:12
for TS being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact holds
TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is regular ;

theorem :: COMPTS_1:13
for TS being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact holds
TS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is normal ;

theorem :: COMPTS_1:14
for T being ( ( ) ( ) TopStruct )
for S being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st T : ( ( ) ( ) TopStruct ) is compact & f : ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & rng f : ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
S : ( ( non empty ) ( non empty ) TopStruct ) is compact ;

theorem :: COMPTS_1:15
for T being ( ( ) ( ) TopStruct )
for P being ( ( ) ( ) Subset of )
for S being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & rng f : ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & P : ( ( ) ( ) Subset of ) is compact holds
f : ( ( Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b3 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is compact ;

theorem :: COMPTS_1:16
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for SS being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is compact & SS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & rng f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] SS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
for PS being ( ( ) ( ) Subset of ) st PS : ( ( ) ( ) Subset of ) is closed holds
f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: PS : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: COMPTS_1:17
for TS being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for SS being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is compact & SS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & dom f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] TS : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non proper open closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] SS : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
f : ( ( Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

definition
let D be ( ( ) ( ) set ) ;
func 1TopSp D -> ( ( ) ( ) TopStruct ) equals :: COMPTS_1:def 5
 TopStruct(# D : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,([#] (bool D : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Element of bool (bool D : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty non proper ) Element of bool (bool D : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Element of bool (bool D : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) ;
end;

registration
let D be ( ( ) ( ) set ) ;
cluster 1TopSp D : ( ( ) ( ) set ) : ( ( ) ( ) TopStruct ) -> strict TopSpace-like ;
end;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
cluster 1TopSp D : ( ( non empty ) ( non empty ) set ) : ( ( ) ( strict TopSpace-like ) TopStruct ) -> non empty ;
end;

registration
let x be ( ( ) ( ) set ) ;
cluster 1TopSp {x : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) -> T_2 ;
end;

registration
cluster non empty TopSpace-like T_2 for ( ( ) ( ) TopStruct ) ;
end;

registration
let T be ( ( non empty TopSpace-like T_2 ) ( non empty TopSpace-like T_0 T_1 T_2 ) TopSpace) ;
cluster compact -> closed for ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let A be ( ( finite ) ( finite ) set ) ;
cluster 1TopSp A : ( ( finite ) ( finite ) set ) : ( ( ) ( strict TopSpace-like ) TopStruct ) -> finite ;
end;

registration
cluster non empty finite strict TopSpace-like for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster finite TopSpace-like -> TopSpace-like compact for ( ( ) ( ) TopStruct ) ;
end;

theorem :: COMPTS_1:18
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) is finite holds
T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is compact ;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster finite -> compact for ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster non empty compact for ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster empty -> T_2 for ( ( ) ( ) TopStruct ) ;
end;

registration
let T be ( ( T_2 ) ( T_0 T_1 T_2 ) TopStruct ) ;
cluster -> T_2 for ( ( ) ( ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ;
end;

theorem :: COMPTS_1:19
for X being ( ( ) ( ) TopStruct )
for Y being ( ( ) ( ) SubSpace of X : ( ( ) ( ) TopStruct ) )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is compact iff B : ( ( ) ( ) Subset of ) is compact ) ;

theorem :: COMPTS_1:20
for T, S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for T1, T2 being ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for f being ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st ([#] T1 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ ([#] T2 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ([#] T1 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ ([#] T2 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) & T1 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is compact & T2 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is compact & T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & f : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & g : ( ( Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & f : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
f : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) +* g : ( ( Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b5 : ( ( ) ( TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( Function-like V21( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: COMPTS_1:21
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T1, T2 being ( ( ) ( TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for p1, p2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st ([#] T1 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ ([#] T2 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ([#] T1 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ ([#] T2 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non proper open closed ) Element of bool the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {p1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) & T1 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is compact & T2 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is compact & T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_2 & f : ( ( Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & g : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & f : ( ( Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) & f : ( ( Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) . p2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
f : ( ( Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b3 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) +* g : ( ( Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b4 : ( ( ) ( TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( Function-like V21( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V21( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

begin

registration
let S be ( ( ) ( ) TopStruct ) ;
cluster the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> open ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster non empty open for ( ( ) ( ) Element of bool (bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: COMPTS_1:22
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F being ( ( ) ( ) set ) holds
( F : ( ( ) ( ) set ) is ( ( open ) ( open ) Subset-Family of ) iff F : ( ( ) ( ) set ) is ( ( open ) ( open ) Subset-Family of ) ) ;

theorem :: COMPTS_1:23
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) is ( ( compact ) ( compact ) Subset of ) iff X : ( ( ) ( ) set ) is ( ( compact ) ( compact ) Subset of ) ) ;