:: WAYBEL26 semantic presentation

begin

notation
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V24(I : ( ( ) ( ) set ) ) RelStr-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V24(I : ( ( ) ( ) set ) ) RelStr-yielding V384() ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
synonym I -POS_prod J for product J;
end;

notation
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V24(I : ( ( ) ( ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V24(I : ( ( ) ( ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
synonym I -TOP_prod J for product J;
end;

definition
let X, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func oContMaps (X,Y) -> ( ( non empty strict ) ( non empty strict ) RelStr ) equals :: WAYBEL26:def 1
 ContMaps (X : ( ( ) ( ) TopRelStr ) ,(Omega Y : ( ( ) ( ) NetStr over X : ( ( ) ( ) TopRelStr ) ) ) : ( ( strict ) ( strict ) TopRelStr ) ) : ( ( strict ) ( strict ) RelStr ) ;
end;

registration
let X, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty strict ) ( non empty strict ) RelStr ) -> non empty constituted-Functions strict reflexive transitive ;
end;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let Y be ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopSpace) ;
cluster oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,Y : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopStruct ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) -> non empty strict antisymmetric ;
end;

theorem :: WAYBEL26:1
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) is ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) set ) is ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) ) ;

theorem :: WAYBEL26:2
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) is ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) set ) is ( ( Function-like quasi_total 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 non empty V24( 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 ) ) ) ;

theorem :: WAYBEL26:3
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a, b being ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) )
for f, g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st a : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & b : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) <= b : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) iff f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Omega b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive strict ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ;

definition
let X, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let A be ( ( ) ( ) Subset of ) ;
:: original: pi
redefine func pi (A,x) -> ( ( ) ( ) Subset of ) ;
end;

registration
let X, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( ) set ) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
cluster pi (A : ( ( non empty ) ( non empty ) Element of bool the carrier of (oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: WAYBEL26:4
Omega Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict satisfying_axiom_of_approximation continuous ) TopRelStr ) is ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) TopAugmentation of BoolePoset 1 : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() directed up-complete /\-complete V354() V361() V362() V363() ) RelStr ) ) ;

theorem :: WAYBEL26:5
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic & ( for V being ( ( open ) ( open ) Subset of ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) . V : ( ( open ) ( open ) Subset of ) : ( ( ) ( ) set ) = chi (V : ( ( open ) ( open ) Subset of ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined {{} : ( ( ) ( Function-like functional empty finite V45() ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,{{} : ( ( ) ( Function-like functional empty finite V45() ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL26:6
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds InclPoset the topology of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) , oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) are_isomorphic ;

definition
let X, Y, Z be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
func oContMaps (X,f) -> ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: WAYBEL26:def 2
 for g being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) -valued Function-like non empty V24( the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total continuous ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds it : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = f : ( ( non empty ) ( non empty ) Element of bool the carrier of (oContMaps (X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of Z : ( ( 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 ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
func oContMaps (f,X) -> ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (Z : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,X : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (Z : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: WAYBEL26:def 3
 for g being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty V24( the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total continuous ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds it : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( non empty ) ( non empty ) Element of bool the carrier of (oContMaps (X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) : ( ( non empty strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier of Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL26:7
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) holds oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is up-complete ;

theorem :: WAYBEL26:8
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) holds oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ;

theorem :: WAYBEL26:9
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 ) ) st f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 ) ) is idempotent holds
oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is idempotent ;

theorem :: WAYBEL26:10
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) holds oContMaps (f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) ,X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ;

theorem :: WAYBEL26:11
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 ) ) st f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 ) ) is idempotent holds
oContMaps (f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( 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 non empty V24( 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 ) ) ,X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is idempotent ;

theorem :: WAYBEL26:12
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds pi (((oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) = f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) .: (pi (A : ( ( ) ( ) Subset of ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL26:13
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y, Z being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving ;

theorem :: WAYBEL26:14
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds pi (((oContMaps (f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) ,X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) = pi (A : ( ( ) ( ) Subset of ) ,(f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL26:15
for Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for X being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace)
for f being ( ( Function-like quasi_total 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 non empty V24( 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 ) ) holds oContMaps (f : ( ( Function-like quasi_total 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 non empty V24( 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 ) ) ,X : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving ;

theorem :: WAYBEL26:16
for X, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) is ( ( full ) ( reflexive transitive antisymmetric full ) SubRelStr of oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) ) ;

theorem :: WAYBEL26:17
for Z being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace)
for Y being ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_a_retraction holds
Omega Y : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b1 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( strict ) ( non empty TopSpace-like reflexive transitive antisymmetric strict ) TopRelStr ) is ( ( directed-sups-inheriting ) ( directed-sups-inheriting ) SubRelStr of Omega Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( strict ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete strict ) TopRelStr ) ) ;

theorem :: WAYBEL26:18
errorfrm ;

theorem :: WAYBEL26:19
errorfrm ;

theorem :: WAYBEL26:20
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) st f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) is being_homeomorphism holds
oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic ;

theorem :: WAYBEL26:21
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) are_homeomorphic holds
oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) , oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) are_isomorphic ;

theorem :: WAYBEL26:22
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Z being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace)
for Y being ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) st Y : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) is_a_retract_of Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous holds
( oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty ) ( non empty TopSpace-like T_0 ) SubSpace of b2 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous ) ;

theorem :: WAYBEL26:23
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y, Z being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) st Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) is_Retract_of Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Z : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous holds
( oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous ) ;

theorem :: WAYBEL26:24
for Y being ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) st not Y : ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) is T_1 holds
Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) is_Retract_of Y : ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) ;

theorem :: WAYBEL26:25
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) st oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is with_suprema holds
not Y : ( ( non empty non trivial TopSpace-like T_0 ) ( non empty non trivial TopSpace-like T_0 ) T_0-TopSpace) is T_1 ;

registration
cluster Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) -> non trivial strict monotone-convergence ;
end;

registration
cluster non empty non trivial TopSpace-like T_0 injective monotone-convergence for ( ( ) ( ) TopStruct ) ;
end;

theorem :: WAYBEL26:26
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty non trivial TopSpace-like T_0 monotone-convergence ) ( non empty non trivial TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) st oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty non trivial TopSpace-like T_0 monotone-convergence ) ( non empty non trivial TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty non trivial TopSpace-like T_0 monotone-convergence ) ( non empty non trivial TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous holds
InclPoset the topology of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) is continuous ;

theorem :: WAYBEL26:27
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for Y being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ex F being ( ( Function-like quasi_total directed-sups-preserving projection ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone directed-sups-preserving projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( ( for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) holds F : ( ( Function-like quasi_total directed-sups-preserving projection ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone directed-sups-preserving projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . f : ( ( Function-like quasi_total continuous ) ( 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 Function-like non empty V24( 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 ) ) : ( ( ) ( ) set ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> (f : ( ( Function-like quasi_total continuous ) ( 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 Function-like non empty V24( 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 ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & ex h being ( ( Function-like quasi_total continuous ) ( 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 Function-like non empty V24( 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 ) ) st
( h : ( ( Function-like quasi_total continuous ) ( 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 Function-like non empty V24( 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 ) ) = X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) --> x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( 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 Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of bool [: the carrier of b1 : ( ( 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 ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & F : ( ( Function-like quasi_total directed-sups-preserving projection ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone directed-sups-preserving projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = oContMaps (h : ( ( Function-like quasi_total continuous ) ( 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 Function-like non empty V24( 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 ) ) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL26:28
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) st oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous holds
( Omega Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( strict ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete strict ) TopRelStr ) is complete & Omega Y : ( ( non empty TopSpace-like T_0 monotone-convergence ) ( non empty TopSpace-like T_0 monotone-convergence ) T_0-TopSpace) : ( ( strict ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete strict ) TopRelStr ) is continuous ) ;

theorem :: WAYBEL26:29
for X being ( ( non empty ) ( non empty ) 1-sorted )
for I being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds (commute f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding ) set ) . i : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) = (proj (J : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like V24(b2 : ( ( non empty ) ( non empty ) set ) ) V384() non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL26:30
for S being ( ( ) ( ) 1-sorted )
for M being ( ( ) ( ) set ) holds Carrier (M : ( ( ) ( ) set ) --> S : ( ( ) ( ) 1-sorted ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b1 : ( ( ) ( ) 1-sorted ) } : ( ( ) ( non empty finite ) set ) -valued Function-like V24(b2 : ( ( ) ( ) set ) ) quasi_total V384() ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b1 : ( ( ) ( ) 1-sorted ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like V24(b2 : ( ( ) ( ) set ) ) ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like V24(b2 : ( ( ) ( ) set ) ) ) set ) = M : ( ( ) ( ) set ) --> the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined { the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) -valued Function-like V24(b2 : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{ the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL26:31
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b3 : ( ( non empty ) ( non empty ) set ) --> b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b3 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) holds commute f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b3 : ( ( non empty ) ( non empty ) set ) --> b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b3 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding ) set ) is ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of M : ( ( non empty ) ( non empty ) set ) , the carrier of (oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL26:32
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds the carrier of (oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) c= Funcs ( the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of 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 ) ) ;

theorem :: WAYBEL26:33
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of M : ( ( non empty ) ( non empty ) set ) , the carrier of (oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) holds commute f : ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total ) Function of b3 : ( ( non empty ) ( non empty ) set ) , the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding ) set ) is ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b3 : ( ( non empty ) ( non empty ) set ) --> b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b3 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b3 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) ;

theorem :: WAYBEL26:34
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty ) ( non empty ) set ) ex F being ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -POS_prod (b2 : ( ( non empty ) ( non empty ) set ) --> (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( functional non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) st
( F : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -POS_prod (b2 : ( ( non empty ) ( non empty ) set ) --> (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( functional non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) is isomorphic & ( for f being ( ( Function-like quasi_total 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 ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) holds F : ( ( Function-like quasi_total ) ( Relation-like the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( non empty ) ( non empty ) set ) -POS_prod (b2 : ( ( non empty ) ( non empty ) set ) --> (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( functional non empty ) set ) -valued Function-like non empty V24( the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(b2 : ( ( non empty ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . f : ( ( Function-like quasi_total 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 ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) : ( ( ) ( Relation-like Function-like ) set ) = commute f : ( ( Function-like quasi_total 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 ) ( non empty ) set ) -TOP_prod (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding ) set ) ) ) ;

theorem :: WAYBEL26:35
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty ) ( non empty ) set ) holds oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(M : ( ( non empty ) ( non empty ) set ) -TOP_prod (M : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total V384() non-Empty TopStruct-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) ,M : ( ( non empty ) ( non empty ) set ) -POS_prod (M : ( ( non empty ) ( non empty ) set ) --> (oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) -valued Function-like non empty V24(b2 : ( ( non empty ) ( non empty ) set ) ) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding ) Element of bool [:b2 : ( ( non empty ) ( non empty ) set ) ,{(oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Sierpinski_Space : ( ( strict ) ( non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence ) TopStruct ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) are_isomorphic ;

theorem :: WAYBEL26:36
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st InclPoset the topology of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) is continuous holds
for Y being ( ( non empty TopSpace-like T_0 injective ) ( non empty TopSpace-like T_0 injective monotone-convergence ) T_0-TopSpace) holds
( oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 injective ) ( non empty TopSpace-like T_0 injective monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,Y : ( ( non empty TopSpace-like T_0 injective ) ( non empty TopSpace-like T_0 injective monotone-convergence ) T_0-TopSpace) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous ) ;

registration
cluster non empty non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott for ( ( ) ( ) TopRelStr ) ;
end;

theorem :: WAYBEL26:37
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for L being ( ( non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty non trivial TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott ) TopLattice) holds
( oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,L : ( ( non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty non trivial TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott ) TopLattice) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is complete & oContMaps (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,L : ( ( non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty non trivial TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott ) TopLattice) ) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) is continuous iff ( InclPoset the topology of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) is continuous & L : ( ( non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty non trivial TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott ) TopLattice) is continuous ) ) ;

registration
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
cluster Union (disjoin f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) -> Relation-like ;
end;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func *graph f -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: WAYBEL26:def 4
(Union (disjoin f : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;
end;

theorem :: WAYBEL26:38
for x, y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V33() ) set ) in *graph f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like ) Relation) iff ( x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: WAYBEL26:39
for X being ( ( finite ) ( finite ) set ) holds
( proj1 X : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) is finite & proj2 X : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) is finite ) ;

theorem :: WAYBEL26:40
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st *graph f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like ) Relation) is ( ( open ) ( open ) Subset of ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

definition
let W be ( ( Relation-like ) ( Relation-like ) Relation) ;
let X be ( ( ) ( ) set ) ;
func (W,X) *graph -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: WAYBEL26:def 5
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Im (W : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: WAYBEL26:41
for W being ( ( Relation-like ) ( Relation-like ) Relation)
for X being ( ( ) ( ) set ) st dom W : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
*graph ((W : ( ( Relation-like ) ( Relation-like ) Relation) ,X : ( ( ) ( ) set ) ) *graph) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like ) Relation) = W : ( ( Relation-like ) ( Relation-like ) Relation) ;

registration
let X, Y be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster -> Relation-like for ( ( ) ( ) Element of bool the carrier of [:X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
cluster -> Relation-like for ( ( ) ( ) Element of the topology of [:X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:X : ( ( ) ( ) set ) ,Y : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: WAYBEL26:42
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for W being ( ( open ) ( Relation-like open ) Subset of )
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds Im (W : ( ( open ) ( Relation-like open ) Subset of ) ,x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) is ( ( open ) ( open ) Subset of ) ;

theorem :: WAYBEL26:43
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) )
for W being ( ( open ) ( Relation-like open ) Subset of ) holds (W : ( ( open ) ( Relation-like open ) Subset of ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) *graph : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( 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 ) ) ;

theorem :: WAYBEL26:44
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) )
for W1, W2 being ( ( open ) ( Relation-like open ) Subset of ) st W1 : ( ( open ) ( Relation-like open ) Subset of ) c= W2 : ( ( open ) ( Relation-like open ) Subset of ) holds
for f1, f2 being ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) st f1 : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = (W1 : ( ( open ) ( Relation-like open ) Subset of ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) *graph : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) & f2 : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = (W2 : ( ( open ) ( Relation-like open ) Subset of ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) *graph : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
f1 : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) <= f2 : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL26:45
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) ex F being ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) st
( F : ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) is monotone & ( for W being ( ( open ) ( Relation-like open ) Subset of ) holds F : ( ( Function-like quasi_total ) ( Relation-like the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) -defined the carrier of (oContMaps (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b3 : ( ( Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott monotone-convergence ) TopAugmentation of InclPoset the topology of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) ) )) : ( ( non empty strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total ) Function of ( ( ) ( non empty non trivial ) set ) , ( ( ) ( non empty ) set ) ) . W : ( ( open ) ( Relation-like open ) Subset of ) : ( ( ) ( ) set ) = (W : ( ( open ) ( Relation-like open ) Subset of ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) *graph : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) ) ;