:: T_0TOPSP semantic presentation

begin

theorem :: T_0TOPSP:1
for X, Y being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V38(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st ( for x1, x2 being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) st x1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V38(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) . x1 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V38(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) . x2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) holds
x2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V38(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) " (f : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V38(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K10(b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K10(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

definition
let T, S be ( ( ) ( ) TopStruct ) ;
pred T,S are_homeomorphic means :: T_0TOPSP:def 1
 ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism ;
end;

definition
let T, S be ( ( ) ( ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr f is open means :: T_0TOPSP:def 2
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
f : ( ( ) ( ) Element of T : ( ( ) ( ) TopStruct ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of S : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is open ;
end;

definition
let T be ( ( non empty ) ( non empty ) TopStruct ) ;
func Indiscernibility T -> ( ( V38( the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) symmetric transitive ) ( Relation-like the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued V38( the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) means :: T_0TOPSP:def 3
 for p, q being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
( [p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of K10(K10(T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
( p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) iff q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) ) );
end;

definition
let T be ( ( non empty ) ( non empty ) TopStruct ) ;
func Indiscernible T -> ( ( non empty ) ( non empty V4() ) a_partition of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) equals :: T_0TOPSP:def 4
 Class (Indiscernibility T : ( ( ) ( ) TopStruct ) ) : ( ( V38( the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) symmetric transitive ) ( Relation-like the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued V38( the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( V4() ) a_partition of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) ;
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func T_0-reflex T -> ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) equals :: T_0TOPSP:def 5
 space (Indiscernible T : ( ( ) ( ) TopStruct ) ) : ( ( non empty ) ( non empty V4() ) a_partition of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster T_0-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) -> non empty TopSpace-like ;
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func T_0-canonical_map T -> ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of (T_0-reflex T : ( ( ) ( ) set ) ) : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V38( the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total continuous ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) equals :: T_0TOPSP:def 6
 Proj (Indiscernible T : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty V4() ) a_partition of the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of (space (Indiscernible T : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty V4() ) a_partition of the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V38( the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total continuous ) Element of K10(K11( the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of (space (Indiscernible T : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty V4() ) a_partition of the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: T_0TOPSP:2
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Subset of ) holds
( V : ( ( ) ( ) Subset of ) is open iff union V : ( ( ) ( ) Subset of ) : ( ( ) ( ) set ) in the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: T_0TOPSP:3
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for C being ( ( ) ( ) set ) holds
( C : ( ( ) ( ) set ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) iff ex p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st C : ( ( ) ( ) set ) = Class ((Indiscernibility T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like the carrier of b1 : ( ( 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 V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: T_0TOPSP:4
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) = Class ((Indiscernibility T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like the carrier of b1 : ( ( 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 V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: T_0TOPSP:5
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) = (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) iff [q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of K192(b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) in Indiscernibility T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like the carrier of b1 : ( ( 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 V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) ) ;

theorem :: T_0TOPSP:6
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) = (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) ;

theorem :: T_0TOPSP:7
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
for C being ( ( ) ( ) Subset of ) st C : ( ( ) ( ) Subset of ) in Indiscernible T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty ) ( non empty V4() ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) & C : ( ( ) ( ) Subset of ) meets A : ( ( ) ( ) Subset of ) holds
C : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) ;

theorem :: T_0TOPSP:8
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open ;

definition
let T be ( ( ) ( ) TopStruct ) ;
redefine attr T is T_0 means :: T_0TOPSP:def 7
( T : ( ( ) ( ) set ) is empty or for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) <> y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
ex V being ( ( ) ( ) Subset of ) st
( V : ( ( ) ( ) Subset of ) is open & ( ( x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) & not y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) ) or ( y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) & not x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) ) ) ) );
end;

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

definition
mode T_0-TopSpace is ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopSpace) ;
end;

theorem :: T_0TOPSP:9
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds T_0-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) ;

theorem :: T_0TOPSP:10
for T, S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st ex h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * (T_0-canonical_map S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K10(K11( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) are_fiberwise_equipotent ) holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) are_homeomorphic ;

theorem :: T_0TOPSP:11
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T0 being ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st [p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of K192(b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) in Indiscernibility T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like the carrier of b1 : ( ( 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 V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) holds
f : ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: T_0TOPSP:12
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T0 being ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: (Class ((Indiscernibility T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like the carrier of b1 : ( ( 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 V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {(f : ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) ;

theorem :: T_0TOPSP:13
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T0 being ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ex h being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * (T_0-canonical_map T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_0-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty 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 T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V38( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of K10(K11( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;