K99() is Element of bool K95()
K95() is set
bool K95() is non empty set
K54() is set
bool K54() is non empty set
bool K99() is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
K96() is set
K97() is set
K98() is set
[:K95(),K95():] is set
bool [:K95(),K95():] is non empty set
K407() is non empty V113() L9()
the carrier of K407() is non empty set
<REAL,+> is non empty V113() V135() V136() associative commutative left-invertible right-invertible V191() left-cancelable right-cancelable V194() L9()
K413() is non empty V113() associative commutative left-cancelable right-cancelable V194() SubStr of <REAL,+>
<NAT,+> is non empty V113() V135() associative commutative left-cancelable right-cancelable V194() uniquely-decomposable SubStr of K413()
<REAL,*> is non empty V113() V135() associative commutative L9()
<NAT,*> is non empty V113() V135() associative commutative uniquely-decomposable SubStr of <REAL,*>
{} is Function-like functional empty finite V45() set
the Function-like functional empty finite V45() set is Function-like functional empty finite V45() set
1 is non empty set
{{},1} is non empty finite set
K722() is set
{{}} is non empty finite V45() set
K378({{}}) is M19({{}})
[:K378({{}}),{{}}:] is set
bool [:K378({{}}),{{}}:] is non empty set
K39(K378({{}}),{{}}) is set
union {} is finite set
Sierpinski_Space is non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence TopStruct
0 is Function-like functional empty finite V45() Element of K99()
{0,1} is non empty finite set
{1} is non empty finite set
{{},{1},{0,1}} is non empty finite set
BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() directed up-complete /\-complete V354() V361() V362() V363() RelStr
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
the carrier of Sierpinski_Space is non empty set
bool the carrier of Sierpinski_Space is non empty set
bool (bool the carrier of Sierpinski_Space) is non empty set
bool 1 is non empty Element of bool (bool 1)
bool 1 is non empty set
bool (bool 1) is non empty set
id Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
[: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is non empty set
id the carrier of Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like one-to-one non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
X is set
X is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty strict RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
S is set
F is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
S is set
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
S is Relation-like Function-like Element of the carrier of (X,Y)
F is Relation-like Function-like Element of the carrier of (X,Y)
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
F is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
W is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
y is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
W1 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
S is Element of the carrier of X
F is Element of bool the carrier of (X,Y)
pi (F,S) is set
the carrier of (Omega Y) is non empty set
bool the carrier of (Omega Y) is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
W is Element of bool the carrier of ((Omega Y) |^ the carrier of X)
pi (W,S) is Element of bool the carrier of (Omega Y)
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
S is set
F is non empty Element of bool the carrier of (X,Y)
pi (F,S) is set
the carrier of X is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
W is non empty Element of bool the carrier of ((Omega Y) |^ the carrier of X)
pi (W,S) is non empty set
Omega Sierpinski_Space is 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
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 #) is strict RelStr
InclPoset (bool 1) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (BoolePoset 1) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1) is non empty set
Omega the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict TopRelStr
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
the carrier of (InclPoset the topology of X) is non empty non trivial set
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,Sierpinski_Space) is non empty set
[: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
[: the carrier of X,{{},1}:] is non empty set
bool [: the carrier of X,{{},1}:] is non empty set
Y is Relation-like Function-like set
proj1 Y is set
proj2 Y is set
S is set
F is set
Y . F is set
F is Element of bool the carrier of X
chi (F, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
[: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
F is Element of the carrier of (InclPoset the topology of X)
W is Element of the carrier of (InclPoset the topology of X)
y is open Element of bool the carrier of X
chi (y, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W1 is open Element of bool the carrier of X
chi (W1, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
F is Relation-like the carrier of (InclPoset the topology of X) -defined the carrier of (X,Sierpinski_Space) -valued Function-like non empty V24( the carrier of (InclPoset the topology of X)) quasi_total Element of bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):]
F . F is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
F . W is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
[: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
the carrier of (Omega Sierpinski_Space) is non empty set
[: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
x is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
g1x is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
rng F is Element of bool the carrier of (X,Sierpinski_Space)
bool the carrier of (X,Sierpinski_Space) is non empty set
y is set
[#] Sierpinski_Space is non empty non proper closed Element of bool the carrier of Sierpinski_Space
W1 is Relation-like the carrier of X -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Sierpinski_Space:]
W is open Element of bool the carrier of Sierpinski_Space
W1 " W is Element of bool the carrier of X
chi ((W1 " W), the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
j is Element of the carrier of X
W1 . j is Element of the carrier of Sierpinski_Space
W2 is Relation-like the carrier of X -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Sierpinski_Space:]
W2 . j is Element of the carrier of Sierpinski_Space
F . (W1 " W) is set
W is Element of the carrier of (InclPoset the topology of X)
F . W is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
y is Element of the carrier of (InclPoset the topology of X)
F . y is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
W1 is Element of bool the carrier of X
chi (W1, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W2 is Element of bool the carrier of X
chi (W2, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W is open Element of bool the carrier of X
F . W is set
chi (W, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset the topology of X) is non empty non trivial set
the carrier of (X,Sierpinski_Space) is non empty set
[: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
Y is Relation-like the carrier of (InclPoset the topology of X) -defined the carrier of (X,Sierpinski_Space) -valued Function-like non empty V24( the carrier of (InclPoset the topology of X)) quasi_total Element of bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
F is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
W is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
y is Relation-like Function-like Element of the carrier of (X,Y)
F . y is Relation-like Function-like Element of the carrier of (X,S)
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
W . y is Relation-like Function-like Element of the carrier of (X,S)
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
W is set
y is set
F . y is set
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W1 (#) F is Relation-like Function-like set
F * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
W is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
y is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W . y is set
F * y is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
y (#) F is Relation-like Function-like set
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (S,X) is non empty set
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
F is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
W is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
y is Relation-like Function-like Element of the carrier of (S,X)
F . y is Relation-like Function-like Element of the carrier of (Y,X)
W1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
W . y is Relation-like Function-like Element of the carrier of (Y,X)
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
W is set
y is set
F . y is set
W1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
F (#) W1 is Relation-like Function-like set
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
W is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
y is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
W . y is set
y * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
F (#) y is Relation-like Function-like set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of X is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
F is Relation-like Function-like Element of the carrier of (X,Y)
W is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,S,F) . F is Relation-like Function-like Element of the carrier of (X,S)
(X,Y,S,F) . W is Relation-like Function-like Element of the carrier of (X,S)
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega S) is non empty set
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
W1 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
y is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
y * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of (Omega S) -valued the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
y * W2 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of (Omega S) -valued the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
g2x is set
a is Element of the carrier of X
(y * W2) . a is Element of the carrier of (Omega S)
W2 . a is Element of the carrier of (Omega Y)
y . (W2 . a) is Element of the carrier of (Omega S)
W1 . a is Element of the carrier of (Omega Y)
(y * W1) . a is Element of the carrier of (Omega S)
y . (W1 . a) is Element of the carrier of (Omega S)
b is Element of the carrier of (Omega Y)
A is Element of the carrier of (Omega Y)
(y * W1) . g2x is set
(y * W2) . g2x is set
x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
g1x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
X is non empty TopSpace-like TopStruct
S is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(X,Y,Y,S) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) * (X,Y,Y,S) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
((X,Y,Y,S) * (X,Y,Y,S)) . F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) . F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) . ((X,Y,Y,S) . F) is Relation-like Function-like Element of the carrier of (X,Y)
W is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
S * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
(X,Y,Y,S) . (S * W) is set
S * (S * W) is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
S * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(S * S) * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
the carrier of (S,X) is non empty set
the carrier of (Y,X) is non empty set
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
F is Relation-like Function-like Element of the carrier of (S,X)
W is Relation-like Function-like Element of the carrier of (S,X)
(X,Y,S,F) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,S,F) . W is Relation-like Function-like Element of the carrier of (Y,X)
the carrier of (Omega X) is non empty set
[: the carrier of S, the carrier of (Omega X):] is non empty set
bool [: the carrier of S, the carrier of (Omega X):] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Omega S) is non empty set
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
W1 is Relation-like the carrier of S -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of (Omega X):]
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
j is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
j (#) W1 is Relation-like Function-like set
y is Relation-like the carrier of S -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of (Omega X):]
j (#) y is Relation-like Function-like set
[: the carrier of Y, the carrier of (Omega X):] is non empty set
bool [: the carrier of Y, the carrier of (Omega X):] is non empty set
g2x is set
y * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of (Omega X) -valued the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of (Omega X):]
a is Element of the carrier of Y
(y * F) . a is Element of the carrier of (Omega X)
F . a is Element of the carrier of S
y . (F . a) is Element of the carrier of (Omega X)
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of (Omega X) -valued the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of (Omega X):]
(W1 * F) . a is Element of the carrier of (Omega X)
W1 . (F . a) is Element of the carrier of (Omega X)
(y * F) . g2x is set
(W1 * F) . g2x is set
x is Relation-like the carrier of Y -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of (Omega X):]
g1x is Relation-like the carrier of Y -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of (Omega X):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
X is non empty TopSpace-like TopStruct
S is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(X,Y,Y,S) is Relation-like the carrier of (Y,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (Y,X)) quasi_total Element of bool [: the carrier of (Y,X), the carrier of (Y,X):]
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
[: the carrier of (Y,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (Y,X), the carrier of (Y,X):] is non empty set
the carrier of X is non empty set
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) * (X,Y,Y,S) is Relation-like the carrier of (Y,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (Y,X)) quasi_total Element of bool [: the carrier of (Y,X), the carrier of (Y,X):]
((X,Y,Y,S) * (X,Y,Y,S)) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) . ((X,Y,Y,S) . F) is Relation-like Function-like Element of the carrier of (Y,X)
W is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
W * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
(X,Y,Y,S) . (W * S) is set
(W * S) * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
S * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
W * (S * S) is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,S) is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
W is Element of the carrier of X
y is Element of bool the carrier of (X,Y)
(X,Y,S,F) .: y is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
(X,S,W,((X,Y,S,F) .: y)) is Element of bool the carrier of (Omega S)
the carrier of (Omega S) is non empty set
bool the carrier of (Omega S) is non empty set
(X,Y,W,y) is Element of bool the carrier of (Omega Y)
the carrier of (Omega Y) is non empty set
bool the carrier of (Omega Y) is non empty set
F .: (X,Y,W,y) is Element of bool the carrier of S
bool the carrier of S is non empty set
W1 is set
W2 is Relation-like Function-like set
W2 . W is set
j is set
(X,Y,S,F) . j is set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
x . W is Element of the carrier of Y
F . (x . W) is Element of the carrier of S
W1 is set
W2 is set
F . W2 is set
j is Relation-like Function-like set
j . W is set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(X,Y,S,F) . x is set
(F * x) . W is Element of the carrier of S
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool the carrier of (X,Y) is non empty set
F is Element of bool the carrier of (X,Y)
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
"\/" (F,(X,Y)) is Relation-like Function-like Element of the carrier of (X,Y)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
(X,Y,S,F) .: F is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
"\/" (((X,Y,S,F) .: F),(X,S)) is Relation-like Function-like Element of the carrier of (X,S)
(X,Y,S,F) . ("\/" (F,(X,Y))) is Relation-like Function-like Element of the carrier of (X,S)
(Omega S) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
x is non empty directed Element of bool the carrier of (X,Y)
(X,Y,S,F) .: x is non empty Element of bool the carrier of (X,S)
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
a is non empty directed Element of bool the carrier of g2x
j is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of X
the carrier of j is non empty set
bool the carrier of j is non empty set
g1x is non empty directed Element of bool the carrier of (X,S)
the carrier of ((Omega S) |^ the carrier of X) is non empty set
bool the carrier of ((Omega S) |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of X --> (Omega Y) is Relation-like the carrier of X -defined {(Omega Y)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega Y)}:]
{(Omega Y)} is non empty finite set
[: the carrier of X,{(Omega Y)}:] is non empty set
bool [: the carrier of X,{(Omega Y)}:] is non empty set
the carrier of X --> (Omega S) is Relation-like the carrier of X -defined {(Omega S)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega S)}:]
{(Omega S)} is non empty finite set
[: the carrier of X,{(Omega S)}:] is non empty set
bool [: the carrier of X,{(Omega S)}:] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
hh is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of X)
"\/" (hh,((Omega S) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of X)
product ( the carrier of X --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega S))) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> (Omega S)) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega S)))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c1)
the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
product ( the carrier of X --> (Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega Y))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega Y))) is non empty set
b is non empty directed Element of bool the carrier of ((Omega Y) |^ the carrier of X)
"\/" (b,((Omega Y) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
c is Element of the carrier of X
( the carrier of X --> (Omega Y)) . c is non empty reflexive transitive antisymmetric RelStr
c1 is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega Y)))
pi (c1,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega Y)) . c)
( the carrier of X --> (Omega Y)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega Y)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega Y)) . c) is non empty set
( the carrier of X --> (Omega S)) . c is non empty reflexive transitive antisymmetric RelStr
b is non empty directed Element of bool the carrier of (Omega Y)
"\/" (c1,(product ( the carrier of X --> (Omega Y)))) is Relation-like Function-like Element of the carrier of (product ( the carrier of X --> (Omega Y)))
("\/" (c1,(product ( the carrier of X --> (Omega Y))))) . c is Element of the carrier of (( the carrier of X --> (Omega Y)) . c)
"\/" ((pi (c1,c)),(( the carrier of X --> (Omega Y)) . c)) is Element of the carrier of (( the carrier of X --> (Omega Y)) . c)
Q is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c)
( the carrier of X --> (Omega S)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
Q .: b is non empty Element of bool the carrier of (Omega S)
W1 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W1 . c is Element of the carrier of (Omega S)
"\/" ((pi (Q,c)),(( the carrier of X --> (Omega S)) . c)) is Element of the carrier of (( the carrier of X --> (Omega S)) . c)
"\/" (b,(Omega Y)) is Element of the carrier of (Omega Y)
F . ("\/" (b,(Omega Y))) is set
W is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(F * W) . c is Element of the carrier of S
W2 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 . c is Element of the carrier of (Omega S)
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (S,X) is non empty set
bool the carrier of (S,X) is non empty set
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
W is Element of the carrier of Y
F . W is Element of the carrier of S
y is Element of bool the carrier of (S,X)
(X,Y,S,F) .: y is Element of bool the carrier of (Y,X)
bool the carrier of (Y,X) is non empty set
(Y,X,W,((X,Y,S,F) .: y)) is Element of bool the carrier of (Omega X)
the carrier of (Omega X) is non empty set
bool the carrier of (Omega X) is non empty set
(S,X,(F . W),y) is Element of bool the carrier of (Omega X)
W1 is set
W2 is Relation-like Function-like set
W2 . W is set
j is set
(X,Y,S,F) . j is set
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
x is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
x * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
x . (F . W) is Element of the carrier of X
W1 is set
W2 is Relation-like Function-like set
W2 . (F . W) is set
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
j is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
j * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
(X,Y,S,F) . j is set
(j * F) . W is Element of the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
(Y,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (Y,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
(S,X,Y,F) is Relation-like the carrier of (Y,S) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (Y,S)) quasi_total Element of bool [: the carrier of (Y,S), the carrier of (X,S):]
the carrier of (Y,S) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (Y,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (Y,S), the carrier of (X,S):] is non empty set
bool the carrier of (Y,S) is non empty set
F is Element of bool the carrier of (Y,S)
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
"\/" (F,(Y,S)) is Relation-like Function-like Element of the carrier of (Y,S)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
(S,X,Y,F) .: F is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
"\/" (((S,X,Y,F) .: F),(X,S)) is Relation-like Function-like Element of the carrier of (X,S)
(S,X,Y,F) . ("\/" (F,(Y,S))) is Relation-like Function-like Element of the carrier of (X,S)
(Omega S) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
x is non empty directed Element of bool the carrier of (Y,S)
(S,X,Y,F) .: x is non empty Element of bool the carrier of (X,S)
(Omega S) |^ the carrier of Y is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of Y
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of ((Omega S) |^ the carrier of Y) is non empty set
bool the carrier of ((Omega S) |^ the carrier of Y) is non empty set
a is non empty directed Element of bool the carrier of g2x
j is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of X
the carrier of j is non empty set
bool the carrier of j is non empty set
g1x is non empty directed Element of bool the carrier of (X,S)
the carrier of ((Omega S) |^ the carrier of X) is non empty set
bool the carrier of ((Omega S) |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of Y --> (Omega S) is Relation-like the carrier of Y -defined {(Omega S)} -valued Function-like non empty V24( the carrier of Y) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of Y,{(Omega S)}:]
{(Omega S)} is non empty finite set
[: the carrier of Y,{(Omega S)}:] is non empty set
bool [: the carrier of Y,{(Omega S)}:] is non empty set
the carrier of X --> (Omega S) is Relation-like the carrier of X -defined {(Omega S)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega S)}:]
[: the carrier of X,{(Omega S)}:] is non empty set
bool [: the carrier of X,{(Omega S)}:] is non empty set
hh is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of X)
"\/" (hh,((Omega S) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of X)
product ( the carrier of X --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega S))) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> (Omega S)) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega S)))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c1)
the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
product ( the carrier of Y --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of Y --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of Y --> (Omega S))) is non empty set
b is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of Y)
"\/" (b,((Omega S) |^ the carrier of Y)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of Y)
c is Element of the carrier of X
F . c is Element of the carrier of Y
( the carrier of Y --> (Omega S)) . (F . c) is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c is non empty reflexive transitive antisymmetric RelStr
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c)
( the carrier of X --> (Omega S)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
c1 is functional non empty directed Element of bool the carrier of (product ( the carrier of Y --> (Omega S)))
pi (c1,(F . c)) is non empty Element of bool the carrier of (( the carrier of Y --> (Omega S)) . (F . c))
( the carrier of Y --> (Omega S)) . (F . c) is non empty reflexive RelStr
the carrier of (( the carrier of Y --> (Omega S)) . (F . c)) is non empty set
bool the carrier of (( the carrier of Y --> (Omega S)) . (F . c)) is non empty set
W1 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W1 . c is Element of the carrier of (Omega S)
"\/" ((pi (Q,c)),(( the carrier of X --> (Omega S)) . c)) is Element of the carrier of (( the carrier of X --> (Omega S)) . c)
"\/" (c1,(product ( the carrier of Y --> (Omega S)))) is Relation-like Function-like Element of the carrier of (product ( the carrier of Y --> (Omega S)))
("\/" (c1,(product ( the carrier of Y --> (Omega S))))) . (F . c) is Element of the carrier of (( the carrier of Y --> (Omega S)) . (F . c))
W is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
W * F is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(W * F) . c is Element of the carrier of S
W2 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 . c is Element of the carrier of (Omega S)
Y is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
S is non empty TopSpace-like SubSpace of Y
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
[#] S is non empty non proper closed Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is non empty set
[#] Y is non empty non proper closed Element of bool the carrier of Y
the carrier of Y is non empty set
bool the carrier of Y is non empty set
the carrier of (X,S) is non empty set
the carrier of (X,Y) is non empty set
W is set
the carrier of X is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
y is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
dom y is Element of bool the carrier of X
bool the carrier of X is non empty set
rng y is Element of bool the carrier of S
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
the InternalRel of (X,S) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Element of bool [: the carrier of (X,S), the carrier of (X,S):]
[: the carrier of (X,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,S), the carrier of (X,S):] is non empty set
the InternalRel of (X,Y) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
W is set
y is set
[W,y] is V33() set
{W,y} is non empty finite set
{W} is non empty finite set
{{W,y},{W}} is non empty finite V45() set
W1 is Relation-like Function-like Element of the carrier of (X,S)
W2 is Relation-like Function-like Element of the carrier of (X,S)
the carrier of X is non empty set
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
j is Relation-like Function-like Element of the carrier of (X,Y)
x is Relation-like Function-like Element of the carrier of (X,Y)
g1x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
g2x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
a is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
b is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
the InternalRel of (X,Y) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
the carrier of (X,Y) is non empty set
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
W is non empty SubRelStr of (X,Y)
the carrier of W is non empty set
the InternalRel of (X,Y) |_2 the carrier of W is Relation-like set
[: the carrier of W, the carrier of W:] is non empty set
the InternalRel of (X,Y) /\ [: the carrier of W, the carrier of W:] is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
the InternalRel of W is Relation-like the carrier of W -defined the carrier of W -valued Element of bool [: the carrier of W, the carrier of W:]
bool [: the carrier of W, the carrier of W:] is non empty set
y is set
W1 is set
[y,W1] is V33() set
{y,W1} is non empty finite set
{y} is non empty finite set
{{y,W1},{y}} is non empty finite V45() set
W2 is Element of the carrier of W
j is Element of the carrier of W
the carrier of X is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
x is Relation-like Function-like Element of the carrier of (X,Y)
g1x is Relation-like Function-like Element of the carrier of (X,Y)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
[x,g1x] is V33() set
{x,g1x} is functional non empty finite set
{x} is functional non empty finite set
{{x,g1x},{x}} is non empty finite V45() set
g2x is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
a is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
b is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
A is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
X is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of X is non empty set
Omega X is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
Y is non empty TopSpace-like T_0 SubSpace of X
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
F is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
S is non empty reflexive transitive antisymmetric up-complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the carrier of (Omega X) is non empty set
the InternalRel of (Omega X) is Relation-like the carrier of (Omega X) -defined the carrier of (Omega X) -valued Element of bool [: the carrier of (Omega X), the carrier of (Omega X):]
[: the carrier of (Omega X), the carrier of (Omega X):] is non empty set
bool [: the carrier of (Omega X), the carrier of (Omega X):] is non empty set
RelStr(# the carrier of (Omega X), the InternalRel of (Omega X) #) is strict RelStr
[#] Y is non empty non proper closed Element of bool the carrier of Y
bool the carrier of Y is non empty set
[#] X is non empty non proper closed Element of bool the carrier of X
bool the carrier of X is non empty set
dom F is Element of bool the carrier of X
rng F is Element of bool the carrier of Y
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
the topology of (Omega X) is non empty Element of bool (bool the carrier of (Omega X))
bool the carrier of (Omega X) is non empty set
bool (bool the carrier of (Omega X)) is non empty set
TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) is non empty strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
W is Relation-like the carrier of (Omega X) -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of (Omega X)) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of (Omega X), the carrier of (Omega X):]
y is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
Image y is non empty strict reflexive transitive antisymmetric full SubRelStr of S
rng y is Element of bool the carrier of S
bool the carrier of S is non empty set
subrelstr (rng y) is strict reflexive transitive antisymmetric full SubRelStr of S
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (subrelstr (rng y)) is set
F is non empty reflexive transitive antisymmetric full SubRelStr of Omega X
X is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like T_0 SubSpace of X
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
S is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of Y is non empty set
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
S is non empty TopSpace-like T_0 SubSpace of Y
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
y is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,y) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
W is non empty reflexive transitive antisymmetric up-complete RelStr
j is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,j) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega j is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega j)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,Y,S,y) | the carrier of (X,S) is Relation-like Function-like set
id (X,S) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like one-to-one non empty V24( the carrier of (X,S)) quasi_total onto bijective idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (X,S), the carrier of (X,S):]
[: the carrier of (X,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,S), the carrier of (X,S):] is non empty set
id the carrier of (X,S) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like one-to-one non empty V24( the carrier of (X,S)) quasi_total Element of bool [: the carrier of (X,S), the carrier of (X,S):]
W2 is non empty reflexive transitive antisymmetric full SubRelStr of W
the carrier of W2 is non empty set
the carrier of W is non empty set
dom y is Element of bool the carrier of Y
bool the carrier of Y is non empty set
rng y is Element of bool the carrier of S
bool the carrier of S is non empty set
x is set
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
g1x is Relation-like Function-like Element of the carrier of (X,Y)
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
g2x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
rng g2x is Element of bool the carrier of Y
y * g2x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
(id (X,S)) . x is set
(X,Y,S,y) . g2x is set
(X,Y,S,y) | the carrier of (X,S) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
((X,Y,S,y) | the carrier of (X,S)) . x is set
dom (id (X,S)) is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
dom ((X,Y,S,y) | the carrier of (X,S)) is Element of bool the carrier of (X,Y)
bool the carrier of (X,Y) is non empty set
(Omega S) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
S is non empty TopSpace-like T_0 SubSpace of Y
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of Y is non empty set
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
[: the carrier of S, the carrier of Y:] is non empty set
bool [: the carrier of S, the carrier of Y:] is non empty set
F /" is Relation-like the carrier of S -defined the carrier of Y -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Y:]
y is Relation-like the carrier of S -defined the carrier of Y -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of Y:]
(X,S,Y,y) is Relation-like the carrier of (X,S) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,S)) quasi_total Element of bool [: the carrier of (X,S), the carrier of (X,Y):]
[: the carrier of (X,S), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,S), the carrier of (X,Y):] is non empty set
rng F is Element of bool the carrier of S
bool the carrier of S is non empty set
[#] S is non empty non proper closed Element of bool the carrier of S
the carrier of X is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
j is Relation-like Function-like Element of the carrier of (X,S)
(X,Y,S,F) * (X,S,Y,y) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,S)) quasi_total Element of bool [: the carrier of (X,S), the carrier of (X,S):]
[: the carrier of (X,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,S), the carrier of (X,S):] is non empty set
((X,Y,S,F) * (X,S,Y,y)) . j is Relation-like Function-like Element of the carrier of (X,S)
(X,S,Y,y) . j is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,S,F) . ((X,S,Y,y) . j) is Relation-like Function-like Element of the carrier of (X,S)
x is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
y * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
(X,Y,S,F) . (y * x) is set
F * (y * x) is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
F * y is Relation-like the carrier of S -defined the carrier of S -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of S) V24( the carrier of S) quasi_total quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
(F * y) * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
(id the carrier of S) * x is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of S:]
id (X,S) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like one-to-one non empty V24( the carrier of (X,S)) quasi_total onto bijective idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (X,S), the carrier of (X,S):]
id the carrier of (X,S) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like one-to-one non empty V24( the carrier of (X,S)) quasi_total Element of bool [: the carrier of (X,S), the carrier of (X,S):]
(id (X,S)) . j is Relation-like Function-like Element of the carrier of (X,S)
dom F is Element of bool the carrier of Y
bool the carrier of Y is non empty set
[#] Y is non empty non proper closed Element of bool the carrier of Y
j is Relation-like Function-like Element of the carrier of (X,Y)
(X,S,Y,y) * (X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
((X,S,Y,y) * (X,Y,S,F)) . j is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,S,F) . j is Relation-like Function-like Element of the carrier of (X,S)
(X,S,Y,y) . ((X,Y,S,F) . j) is Relation-like Function-like Element of the carrier of (X,Y)
x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
(X,S,Y,y) . (F * x) is set
y * (F * x) is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
y * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
(y * F) * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
id the carrier of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like one-to-one non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
(id the carrier of Y) * x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
id (X,Y) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like one-to-one non empty V24( the carrier of (X,Y)) quasi_total onto bijective idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
id the carrier of (X,Y) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like one-to-one non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
(id (X,Y)) . j is Relation-like Function-like Element of the carrier of (X,Y)
Y is non empty TopSpace-like TopStruct
S is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of Y is non empty set
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of S:]
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
S is non empty TopSpace-like T_0 SubSpace of Y
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is non empty TopSpace-like T_0 SubSpace of S
(X,F) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega F is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega F)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
X is non empty non trivial TopSpace-like T_0 TopStruct
the carrier of X is non empty non trivial set
bool the carrier of X is non empty set
Y is Element of the carrier of X
S is Element of the carrier of X
F is Element of bool the carrier of X
F is Element of bool the carrier of X
F is Element of bool the carrier of X
Omega X is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (Omega X) is non empty set
the topology of (Omega X) is non empty Element of bool (bool the carrier of (Omega X))
bool the carrier of (Omega X) is non empty set
bool (bool the carrier of (Omega X)) is non empty set
TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) is non empty strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
F is Element of the carrier of (Omega X)
W is Element of the carrier of (Omega X)
y is open upper Element of bool the carrier of (Omega X)
(0,1) --> (F,W) is Relation-like {0,1} -defined the carrier of (Omega X) -valued Function-like non empty V24({0,1}) quasi_total finite Element of bool [:{0,1}, the carrier of (Omega X):]
[:{0,1}, the carrier of (Omega X):] is non empty set
bool [:{0,1}, the carrier of (Omega X):] is non empty set
[: the carrier of Sierpinski_Space, the carrier of (Omega X):] is non empty set
bool [: the carrier of Sierpinski_Space, the carrier of (Omega X):] is non empty set
[: the carrier of Sierpinski_Space, the carrier of X:] is non empty set
bool [: the carrier of Sierpinski_Space, the carrier of X:] is non empty set
[: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
W1 is open upper Element of bool the carrier of (Omega X)
chi (W1, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
[: the carrier of X,{{},1}:] is non empty set
bool [: the carrier of X,{{},1}:] is non empty set
y is Relation-like the carrier of Sierpinski_Space -defined the carrier of X -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total continuous Element of bool [: the carrier of Sierpinski_Space, the carrier of X:]
W2 is Relation-like the carrier of X -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Sierpinski_Space:]
W2 * y is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of Sierpinski_Space) V24( the carrier of Sierpinski_Space) quasi_total quasi_total continuous Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
X is non empty TopSpace-like TopStruct
Y is non empty non trivial TopSpace-like T_0 TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of Y is non empty non trivial set
S is Element of the carrier of Y
F is Element of the carrier of Y
the carrier of X is non empty set
the Element of the carrier of X is Element of the carrier of X
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
X --> S is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
the carrier of X --> S is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
X --> F is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
the carrier of X --> F is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
W1 is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of W1 is non empty set
W is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
y is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
W2 is Element of the carrier of W1
j is Element of the carrier of W1
W2 "\/" j is Element of the carrier of W1
g1x is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
g1x . the Element of the carrier of X is Element of the carrier of (Omega Y)
g2x is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
g2x . the Element of the carrier of X is Element of the carrier of (Omega Y)
x is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
x . the Element of the carrier of X is Element of the carrier of (Omega Y)
a is Element of the carrier of (Omega Y)
b is Element of the carrier of (Omega Y)
A is Element of the carrier of (Omega Y)
hh is Element of the carrier of (Omega Y)
a is Element of the carrier of (Omega Y)
b is Element of the carrier of (Omega Y)
a is Element of the carrier of (Omega Y)
b is Element of the carrier of (Omega Y)
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
A is Element of the carrier of Y
hh is Element of the carrier of Y
B is Element of bool the carrier of Y
B is Element of bool the carrier of Y
B is open upper Element of bool the carrier of (Omega Y)
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
Y is non empty non trivial TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Element of the carrier of X
X --> Y is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of X:]
the carrier of X --> Y is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,S) is non empty set
[: the carrier of (X,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,S), the carrier of (X,S):] is non empty set
the carrier of S is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
F is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of X:]
(S,X,X,F) is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,S)) quasi_total Element of bool [: the carrier of (X,S), the carrier of (X,S):]
dom F is Element of bool the carrier of X
bool the carrier of X is non empty set
F * F is Relation-like the carrier of X -defined the carrier of X -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of X:]
F . Y is Element of the carrier of X
the carrier of X --> (F . Y) is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
y is Relation-like the carrier of (X,S) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,S)) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of (X,S), the carrier of (X,S):]
W1 is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
dom W1 is Element of bool the carrier of X
y . W1 is set
W1 * ( the carrier of X --> Y) is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of S:]
W1 . Y is Element of the carrier of S
X --> (W1 . Y) is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
the carrier of X --> (W1 . Y) is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of S:]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of X is non empty set
the Element of the carrier of X is Element of the carrier of X
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the carrier of Y is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (X,Y) is non empty set
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
X --> the Element of the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of X:]
the carrier of X --> the Element of the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
F is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
Image F is non empty strict reflexive transitive antisymmetric full SubRelStr of (X,Y)
rng F is Element of bool the carrier of (X,Y)
bool the carrier of (X,Y) is non empty set
subrelstr (rng F) is strict reflexive transitive antisymmetric full SubRelStr of (X,Y)
F is non empty reflexive transitive antisymmetric full SubRelStr of (Omega Y) |^ the carrier of X
the carrier of F is non empty set
dom F is Element of bool the carrier of (X,Y)
W is set
y is set
F . y is set
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W1 . the Element of the carrier of X is Element of the carrier of Y
X --> (W1 . the Element of the carrier of X) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
the carrier of X --> (W1 . the Element of the carrier of X) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
W2 is Element of the carrier of (Omega Y)
the carrier of X --> W2 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
y is Element of the carrier of (Omega Y)
the carrier of X --> y is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
X --> y is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W1 . the Element of the carrier of X is Element of the carrier of Y
X --> (W1 . the Element of the carrier of X) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
the carrier of X --> (W1 . the Element of the carrier of X) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
F . W is set
X is non empty 1-sorted
the carrier of X is non empty set
Y is non empty set
S is Relation-like Y -defined Function-like V24(Y) V384() non-Empty TopStruct-yielding set
product S is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product S) is non empty set
[: the carrier of X, the carrier of (product S):] is non empty set
bool [: the carrier of X, the carrier of (product S):] is non empty set
F is Relation-like the carrier of X -defined the carrier of (product S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (product S):]
commute F is Relation-like Function-like Function-yielding set
Carrier S is Relation-like non-empty Y -defined Function-like V24(Y) set
product (Carrier S) is set
F is Element of Y
(commute F) . F is set
S . F is non empty TopStruct
the carrier of (S . F) is non empty set
proj (S,F) is Relation-like the carrier of (product S) -defined the carrier of (S . F) -valued Function-like non empty V24( the carrier of (product S)) quasi_total Element of bool [: the carrier of (product S), the carrier of (S . F):]
[: the carrier of (product S), the carrier of (S . F):] is non empty set
bool [: the carrier of (product S), the carrier of (S . F):] is non empty set
(proj (S,F)) * F is Relation-like the carrier of X -defined the carrier of (S . F) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (S . F):]
[: the carrier of X, the carrier of (S . F):] is non empty set
bool [: the carrier of X, the carrier of (S . F):] is non empty set
dom (Carrier S) is Element of bool Y
bool Y is non empty set
rng F is Element of bool the carrier of (product S)
bool the carrier of (product S) is non empty set
Union (Carrier S) is set
Funcs (Y,(Union (Carrier S))) is functional set
W is set
y is Relation-like Function-like set
proj1 y is set
proj2 y is set
W1 is set
W2 is set
y . W2 is set
(Carrier S) . W2 is set
dom F is Element of bool the carrier of X
bool the carrier of X is non empty set
Funcs ( the carrier of X,(Funcs (Y,(Union (Carrier S))))) is functional set
Funcs ( the carrier of X,(Union (Carrier S))) is functional set
Funcs (Y,(Funcs ( the carrier of X,(Union (Carrier S))))) is functional set
proj2 (commute F) is set
W is Relation-like Function-like set
proj1 W is set
proj2 W is set
W is Relation-like Function-like set
proj1 W is set
proj2 W is set
W is Relation-like Function-like set
proj1 W is set
proj2 W is set
proj ((Carrier S),F) is Relation-like Function-like set
proj1 (proj ((Carrier S),F)) is set
y is set
W1 is Element of the carrier of X
F . W1 is Relation-like Function-like Element of the carrier of (product S)
W2 is Relation-like Function-like set
proj1 W2 is set
((proj (S,F)) * F) . W1 is Element of the carrier of (S . F)
(proj (S,F)) . (F . W1) is Element of the carrier of (S . F)
(proj ((Carrier S),F)) . (F . W1) is set
W2 . F is set
W . y is set
((proj (S,F)) * F) . y is set
dom ((proj (S,F)) * F) is Element of bool the carrier of X
X is 1-sorted
the carrier of X is set
Y is set
Y --> X is Relation-like Y -defined {X} -valued Function-like V24(Y) quasi_total V384() Element of bool [:Y,{X}:]
{X} is non empty finite set
[:Y,{X}:] is set
bool [:Y,{X}:] is non empty set
Carrier (Y --> X) is Relation-like Y -defined Function-like V24(Y) set
Y --> the carrier of X is Relation-like Y -defined { the carrier of X} -valued Function-like V24(Y) quasi_total Element of bool [:Y,{ the carrier of X}:]
{ the carrier of X} is non empty finite set
[:Y,{ the carrier of X}:] is set
bool [:Y,{ the carrier of X}:] is non empty set
S is set
(Y --> X) . S is set
(Carrier (Y --> X)) . S is set
(Y --> the carrier of X) . S is set
F is 1-sorted
the carrier of F is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
S is non empty set
S --> Y is Relation-like S -defined {Y} -valued Function-like non empty V24(S) quasi_total V384() non-Empty TopStruct-yielding Element of bool [:S,{Y}:]
{Y} is non empty finite set
[:S,{Y}:] is non empty set
bool [:S,{Y}:] is non empty set
product (S --> Y) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product (S --> Y)) is non empty set
[: the carrier of X, the carrier of (product (S --> Y)):] is non empty set
bool [: the carrier of X, the carrier of (product (S --> Y)):] is non empty set
[:S, the carrier of (X,Y):] is non empty set
bool [:S, the carrier of (X,Y):] is non empty set
F is Relation-like the carrier of X -defined the carrier of (product (S --> Y)) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (product (S --> Y)):]
commute F is Relation-like Function-like Function-yielding set
rng F is Element of bool the carrier of (product (S --> Y))
bool the carrier of (product (S --> Y)) is non empty set
the carrier of Y is non empty set
Funcs (S, the carrier of Y) is functional non empty FUNCTION_DOMAIN of S, the carrier of Y
F is set
S --> the carrier of Y is Relation-like S -defined { the carrier of Y} -valued Function-like non empty V24(S) quasi_total Element of bool [:S,{ the carrier of Y}:]
{ the carrier of Y} is non empty finite set
[:S,{ the carrier of Y}:] is non empty set
bool [:S,{ the carrier of Y}:] is non empty set
dom (S --> the carrier of Y) is Element of bool S
bool S is non empty set
Carrier (S --> Y) is Relation-like non-empty S -defined Function-like V24(S) set
product (Carrier (S --> Y)) is set
product (S --> the carrier of Y) is set
W is Relation-like Function-like set
proj1 W is set
proj2 W is set
y is set
W1 is set
W . W1 is set
(S --> the carrier of Y) . W1 is set
dom F is Element of bool the carrier of X
bool the carrier of X is non empty set
Funcs ( the carrier of X,(Funcs (S, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of X, Funcs (S, the carrier of Y)
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
Funcs (S,(Funcs ( the carrier of X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of S, Funcs ( the carrier of X, the carrier of Y)
proj2 (commute F) is set
F is set
proj1 (commute F) is set
W is set
(commute F) . W is set
W1 is Relation-like Function-like set
proj1 W1 is set
proj2 W1 is set
y is Element of S
(S --> Y) . y is non empty TopStruct
the carrier of ((S --> Y) . y) is non empty set
proj ((S --> Y),y) is Relation-like the carrier of (product (S --> Y)) -defined the carrier of ((S --> Y) . y) -valued Function-like non empty V24( the carrier of (product (S --> Y))) quasi_total Element of bool [: the carrier of (product (S --> Y)), the carrier of ((S --> Y) . y):]
[: the carrier of (product (S --> Y)), the carrier of ((S --> Y) . y):] is non empty set
bool [: the carrier of (product (S --> Y)), the carrier of ((S --> Y) . y):] is non empty set
(proj ((S --> Y),y)) * F is Relation-like the carrier of X -defined the carrier of ((S --> Y) . y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ((S --> Y) . y):]
[: the carrier of X, the carrier of ((S --> Y) . y):] is non empty set
bool [: the carrier of X, the carrier of ((S --> Y) . y):] is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
S is non empty set
[:S, the carrier of (X,Y):] is non empty set
bool [:S, the carrier of (X,Y):] is non empty set
S --> Y is Relation-like S -defined {Y} -valued Function-like non empty V24(S) quasi_total V384() non-Empty TopStruct-yielding Element of bool [:S,{Y}:]
{Y} is non empty finite set
[:S,{Y}:] is non empty set
bool [:S,{Y}:] is non empty set
product (S --> Y) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product (S --> Y)) is non empty set
[: the carrier of X, the carrier of (product (S --> Y)):] is non empty set
bool [: the carrier of X, the carrier of (product (S --> Y)):] is non empty set
F is Relation-like S -defined the carrier of (X,Y) -valued Function-like non empty V24(S) quasi_total Element of bool [:S, the carrier of (X,Y):]
commute F is Relation-like Function-like Function-yielding set
bool the carrier of (product (S --> Y)) is non empty set
bool (bool the carrier of (product (S --> Y))) is non empty set
product_prebasis (S --> Y) is Element of bool (bool (product (Carrier (S --> Y))))
Carrier (S --> Y) is Relation-like non-empty S -defined Function-like V24(S) set
product (Carrier (S --> Y)) is set
bool (product (Carrier (S --> Y))) is non empty set
bool (bool (product (Carrier (S --> Y)))) is non empty set
the carrier of Y is non empty set
S --> the carrier of Y is Relation-like S -defined { the carrier of Y} -valued Function-like non empty V24(S) quasi_total Element of bool [:S,{ the carrier of Y}:]
{ the carrier of Y} is non empty finite set
[:S,{ the carrier of Y}:] is non empty set
bool [:S,{ the carrier of Y}:] is non empty set
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
dom F is Element of bool S
bool S is non empty set
rng F is Element of bool the carrier of (X,Y)
bool the carrier of (X,Y) is non empty set
Funcs (S,(Funcs ( the carrier of X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of S, Funcs ( the carrier of X, the carrier of Y)
Funcs (S, the carrier of Y) is functional non empty FUNCTION_DOMAIN of S, the carrier of Y
Funcs ( the carrier of X,(Funcs (S, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of X, Funcs (S, the carrier of Y)
y is Relation-like Function-like set
proj1 y is set
proj2 y is set
y is Element of bool the carrier of (product (S --> Y))
F is open quasi_prebasis Element of bool (bool the carrier of (product (S --> Y)))
W2 is TopStruct
the carrier of W2 is set
bool the carrier of W2 is non empty set
W1 is set
j is Element of bool the carrier of W2
(S --> Y) . W1 is set
(Carrier (S --> Y)) +* (W1,j) is Relation-like Function-like set
product ((Carrier (S --> Y)) +* (W1,j)) is set
x is Element of S
(Carrier (S --> Y)) +* (x,j) is Relation-like Function-like set
proj1 ((Carrier (S --> Y)) +* (x,j)) is set
dom (Carrier (S --> Y)) is Element of bool S
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F . x is Relation-like Function-like Element of the carrier of (X,Y)
((Carrier (S --> Y)) +* (x,j)) . x is set
bool the carrier of X is non empty set
g2x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
g2x " j is Element of bool the carrier of X
a is set
W is Relation-like the carrier of X -defined the carrier of (product (S --> Y)) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (product (S --> Y)):]
W " y is Element of bool the carrier of X
W . a is set
A is Relation-like Function-like set
proj1 A is set
A . x is set
g2x . a is set
b is Element of bool the carrier of X
[#] Y is non empty non proper closed Element of bool the carrier of Y
bool the carrier of Y is non empty set
hh is Element of bool the carrier of X
B is set
W . B is set
rng W is Element of bool the carrier of (product (S --> Y))
B is Relation-like Function-like set
proj1 B is set
proj2 B is set
B is Relation-like Function-like set
proj1 B is set
proj2 B is set
B is Relation-like Function-like set
proj1 B is set
proj2 B is set
g2x . B is set
B is set
(S --> the carrier of Y) . B is set
B . B is set
((Carrier (S --> Y)) +* (x,j)) . B is set
b is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of X is non empty set
Y is non empty set
Y --> Sierpinski_Space is Relation-like Y -defined {Sierpinski_Space} -valued Function-like non empty V24(Y) quasi_total V384() non-Empty TopStruct-yielding Element of bool [:Y,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty finite set
[:Y,{Sierpinski_Space}:] is non empty set
bool [:Y,{Sierpinski_Space}:] is non empty set
product (Y --> Sierpinski_Space) is non empty strict TopSpace-like T_0 constituted-Functions TopStruct
(X,(product (Y --> Sierpinski_Space))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega (product (Y --> Sierpinski_Space)) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega (product (Y --> Sierpinski_Space)))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,(product (Y --> Sierpinski_Space))) is non empty set
Y --> (X,Sierpinski_Space) is Relation-like Y -defined {(X,Sierpinski_Space)} -valued Function-like non empty V24(Y) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding Element of bool [:Y,{(X,Sierpinski_Space)}:]
{(X,Sierpinski_Space)} is non empty finite set
[:Y,{(X,Sierpinski_Space)}:] is non empty set
bool [:Y,{(X,Sierpinski_Space)}:] is non empty set
product (Y --> (X,Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product (Y --> (X,Sierpinski_Space))) is functional non empty set
[: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
the carrier of (product (Y --> Sierpinski_Space)) is non empty set
[: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):] is non empty set
bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):] is non empty set
W1 is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined Function-like V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) set
dom W1 is Element of bool the carrier of (X,(product (Y --> Sierpinski_Space)))
bool the carrier of (X,(product (Y --> Sierpinski_Space))) is non empty set
proj2 W1 is set
W2 is set
j is set
W1 . j is set
x is Relation-like the carrier of X -defined the carrier of (product (Y --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):]
commute x is Relation-like Function-like Function-yielding set
the carrier of (X,Sierpinski_Space) is non empty set
[:Y, the carrier of (X,Sierpinski_Space):] is non empty set
bool [:Y, the carrier of (X,Sierpinski_Space):] is non empty set
g1x is Relation-like Y -defined the carrier of (X,Sierpinski_Space) -valued Function-like non empty V24(Y) quasi_total Element of bool [:Y, the carrier of (X,Sierpinski_Space):]
dom g1x is Element of bool Y
bool Y is non empty set
rng g1x is Element of bool the carrier of (X,Sierpinski_Space)
bool the carrier of (X,Sierpinski_Space) is non empty set
Funcs (Y, the carrier of (X,Sierpinski_Space)) is functional non empty FUNCTION_DOMAIN of Y, the carrier of (X,Sierpinski_Space)
(X,Sierpinski_Space) |^ Y is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of ((X,Sierpinski_Space) |^ Y) is non empty set
j is Relation-like the carrier of (product (Y --> (X,Sierpinski_Space))) -defined Function-like V24( the carrier of (product (Y --> (X,Sierpinski_Space)))) set
dom j is functional Element of bool the carrier of (product (Y --> (X,Sierpinski_Space)))
bool the carrier of (product (Y --> (X,Sierpinski_Space))) is non empty set
proj2 j is set
x is set
g1x is set
j . g1x is set
(X,Sierpinski_Space) |^ Y is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of ((X,Sierpinski_Space) |^ Y) is non empty set
the carrier of (X,Sierpinski_Space) is non empty set
Funcs (Y, the carrier of (X,Sierpinski_Space)) is functional non empty FUNCTION_DOMAIN of Y, the carrier of (X,Sierpinski_Space)
g2x is Relation-like Function-like set
proj1 g2x is set
proj2 g2x is set
[:Y, the carrier of (X,Sierpinski_Space):] is non empty set
bool [:Y, the carrier of (X,Sierpinski_Space):] is non empty set
commute g2x is Relation-like Function-like Function-yielding set
W2 is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined the carrier of (product (Y --> (X,Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):]
Carrier (Y --> Sierpinski_Space) is Relation-like non-empty Y -defined Function-like V24(Y) set
product (Carrier (Y --> Sierpinski_Space)) is set
Y --> the carrier of Sierpinski_Space is Relation-like Y -defined { the carrier of Sierpinski_Space} -valued Function-like non empty V24(Y) quasi_total Element of bool [:Y,{ the carrier of Sierpinski_Space}:]
{ the carrier of Sierpinski_Space} is non empty finite set
[:Y,{ the carrier of Sierpinski_Space}:] is non empty set
bool [:Y,{ the carrier of Sierpinski_Space}:] is non empty set
product (Y --> the carrier of Sierpinski_Space) is set
Funcs (Y, the carrier of Sierpinski_Space) is functional non empty FUNCTION_DOMAIN of Y, the carrier of Sierpinski_Space
[: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):] is non empty set
bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):] is non empty set
Funcs ( the carrier of X, the carrier of (product (Y --> Sierpinski_Space))) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of (product (Y --> Sierpinski_Space))
g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
commute g1x is Relation-like Function-like Function-yielding set
commute (commute g1x) is Relation-like Function-like Function-yielding set
x is Relation-like the carrier of (product (Y --> (X,Sierpinski_Space))) -defined the carrier of (X,(product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (product (Y --> (X,Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):]
x * W2 is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined the carrier of (X,(product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):]
[: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):] is non empty set
bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):] is non empty set
(x * W2) . g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
W2 . g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
x . (W2 . g1x) is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
commute (W2 . g1x) is Relation-like Function-like Function-yielding set
id (X,(product (Y --> Sierpinski_Space))) is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined the carrier of (X,(product (Y --> Sierpinski_Space))) -valued Function-like one-to-one non empty V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) quasi_total onto bijective idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):]
id the carrier of (X,(product (Y --> Sierpinski_Space))) is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined the carrier of (X,(product (Y --> Sierpinski_Space))) -valued Function-like one-to-one non empty V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (X,(product (Y --> Sierpinski_Space))):]
(id (X,(product (Y --> Sierpinski_Space)))) . g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
the carrier of (Omega (product (Y --> Sierpinski_Space))) is non empty set
the InternalRel of (Omega (product (Y --> Sierpinski_Space))) is Relation-like the carrier of (Omega (product (Y --> Sierpinski_Space))) -defined the carrier of (Omega (product (Y --> Sierpinski_Space))) -valued Element of bool [: the carrier of (Omega (product (Y --> Sierpinski_Space))), the carrier of (Omega (product (Y --> Sierpinski_Space))):]
[: the carrier of (Omega (product (Y --> Sierpinski_Space))), the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
bool [: the carrier of (Omega (product (Y --> Sierpinski_Space))), the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
RelStr(# the carrier of (Omega (product (Y --> Sierpinski_Space))), the InternalRel of (Omega (product (Y --> Sierpinski_Space))) #) is strict RelStr
Y --> (Omega Sierpinski_Space) is Relation-like Y -defined {(Omega Sierpinski_Space)} -valued Function-like non empty V24(Y) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [:Y,{(Omega Sierpinski_Space)}:]
{(Omega Sierpinski_Space)} is non empty finite set
[:Y,{(Omega Sierpinski_Space)}:] is non empty set
bool [:Y,{(Omega Sierpinski_Space)}:] is non empty set
product (Y --> (Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
g2x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
W2 . g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
W2 . g2x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
[: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
B is Element of Y
(Y --> (X,Sierpinski_Space)) . B is non empty reflexive transitive antisymmetric RelStr
the carrier of (Omega Sierpinski_Space) is non empty set
[: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
(W2 . g1x) . B is Element of the carrier of ((Y --> (X,Sierpinski_Space)) . B)
(Y --> (X,Sierpinski_Space)) . B is non empty reflexive RelStr
the carrier of ((Y --> (X,Sierpinski_Space)) . B) is non empty set
(W2 . g2x) . B is Element of the carrier of ((Y --> (X,Sierpinski_Space)) . B)
Q is set
hh is Relation-like the carrier of X -defined the carrier of (Omega (product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):]
commute hh is Relation-like Function-like Function-yielding set
B is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
Q is Element of the carrier of X
B . Q is Element of the carrier of (Omega Sierpinski_Space)
b is Relation-like the carrier of X -defined the carrier of (product (Y --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):]
b . Q is Relation-like Function-like Element of the carrier of (product (Y --> Sierpinski_Space))
(b . Q) . B is Element of the carrier of ((Y --> Sierpinski_Space) . B)
(Y --> Sierpinski_Space) . B is non empty TopStruct
the carrier of ((Y --> Sierpinski_Space) . B) is non empty set
the carrier of (product (Y --> (Omega Sierpinski_Space))) is functional non empty set
A is Relation-like the carrier of X -defined the carrier of (Omega (product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):]
A . Q is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
hh . Q is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
commute A is Relation-like Function-like Function-yielding set
B is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
B . Q is Element of the carrier of (Omega Sierpinski_Space)
a is Relation-like the carrier of X -defined the carrier of (product (Y --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):]
a . Q is Relation-like Function-like Element of the carrier of (product (Y --> Sierpinski_Space))
(a . Q) . B is Element of the carrier of ((Y --> Sierpinski_Space) . B)
c1 is Relation-like Function-like Element of the carrier of (product (Y --> (Omega Sierpinski_Space)))
c is Relation-like Function-like Element of the carrier of (product (Y --> (Omega Sierpinski_Space)))
b is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
c9 is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
(Y --> (Omega Sierpinski_Space)) . B is non empty reflexive RelStr
c1 . B is Element of the carrier of ((Y --> (Omega Sierpinski_Space)) . B)
the carrier of ((Y --> (Omega Sierpinski_Space)) . B) is non empty set
c . B is Element of the carrier of ((Y --> (Omega Sierpinski_Space)) . B)
(Y --> (Omega Sierpinski_Space)) . B is non empty reflexive transitive antisymmetric RelStr
B . Q is set
B . Q is set
(X,Sierpinski_Space) |^ Y is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of ((X,Sierpinski_Space) |^ Y) is non empty set
the carrier of (X,Sierpinski_Space) is non empty set
Funcs (Y, the carrier of (X,Sierpinski_Space)) is functional non empty FUNCTION_DOMAIN of Y, the carrier of (X,Sierpinski_Space)
Funcs ( the carrier of X, the carrier of Sierpinski_Space) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Sierpinski_Space
Funcs (Y,(Funcs ( the carrier of X, the carrier of Sierpinski_Space))) is functional non empty FUNCTION_DOMAIN of Y, Funcs ( the carrier of X, the carrier of Sierpinski_Space)
g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
g2x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
x . g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
x . g2x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
[: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):] is non empty set
A is set
the carrier of (product (Y --> (Omega Sierpinski_Space))) is functional non empty set
a is Relation-like the carrier of X -defined the carrier of (Omega (product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):]
hh is Element of the carrier of X
a . hh is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
b is Relation-like the carrier of X -defined the carrier of (Omega (product (Y --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega (product (Y --> Sierpinski_Space))):]
b . hh is Element of the carrier of (Omega (product (Y --> Sierpinski_Space)))
B is Element of Y
(Y --> (X,Sierpinski_Space)) . B is non empty reflexive transitive antisymmetric RelStr
the carrier of (Omega Sierpinski_Space) is non empty set
[: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
g1x . B is Element of the carrier of ((Y --> (X,Sierpinski_Space)) . B)
(Y --> (X,Sierpinski_Space)) . B is non empty reflexive RelStr
the carrier of ((Y --> (X,Sierpinski_Space)) . B) is non empty set
g2x . B is Element of the carrier of ((Y --> (X,Sierpinski_Space)) . B)
Q is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
Q is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
Q . hh is Element of the carrier of (Omega Sierpinski_Space)
Q . hh is Element of the carrier of (Omega Sierpinski_Space)
commute g2x is Relation-like Function-like Function-yielding set
B is Relation-like Function-like Element of the carrier of (product (Y --> (Omega Sierpinski_Space)))
B . B is Element of the carrier of ((Y --> (Omega Sierpinski_Space)) . B)
(Y --> (Omega Sierpinski_Space)) . B is non empty reflexive RelStr
the carrier of ((Y --> (Omega Sierpinski_Space)) . B) is non empty set
commute g1x is Relation-like Function-like Function-yielding set
B is Relation-like Function-like Element of the carrier of (product (Y --> (Omega Sierpinski_Space)))
B . B is Element of the carrier of ((Y --> (Omega Sierpinski_Space)) . B)
c1 is Element of the carrier of (Omega Sierpinski_Space)
c is Element of the carrier of (Omega Sierpinski_Space)
a . A is set
b . A is set
g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
commute g1x is Relation-like Function-like Function-yielding set
commute (commute g1x) is Relation-like Function-like Function-yielding set
W2 * x is Relation-like the carrier of (product (Y --> (X,Sierpinski_Space))) -defined the carrier of (product (Y --> (X,Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (product (Y --> (X,Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):]
[: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
(W2 * x) . g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
x . g1x is Relation-like Function-like Element of the carrier of (X,(product (Y --> Sierpinski_Space)))
W2 . (x . g1x) is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
commute (x . g1x) is Relation-like Function-like Function-yielding set
id (product (Y --> (X,Sierpinski_Space))) is Relation-like the carrier of (product (Y --> (X,Sierpinski_Space))) -defined the carrier of (product (Y --> (X,Sierpinski_Space))) -valued Function-like one-to-one non empty V24( the carrier of (product (Y --> (X,Sierpinski_Space)))) quasi_total onto bijective idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):]
id the carrier of (product (Y --> (X,Sierpinski_Space))) is Relation-like the carrier of (product (Y --> (X,Sierpinski_Space))) -defined the carrier of (product (Y --> (X,Sierpinski_Space))) -valued Function-like one-to-one non empty V24( the carrier of (product (Y --> (X,Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (product (Y --> (X,Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):]
(id (product (Y --> (X,Sierpinski_Space)))) . g1x is Relation-like Function-like Element of the carrier of (product (Y --> (X,Sierpinski_Space)))
g1x is Relation-like the carrier of X -defined the carrier of (product (Y --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):]
W2 . g1x is Relation-like Function-like set
commute g1x is Relation-like Function-like Function-yielding set
X is non empty TopSpace-like TopStruct
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Y is non empty set
Y --> Sierpinski_Space is Relation-like Y -defined {Sierpinski_Space} -valued Function-like non empty V24(Y) quasi_total V384() non-Empty TopStruct-yielding Element of bool [:Y,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty finite set
[:Y,{Sierpinski_Space}:] is non empty set
bool [:Y,{Sierpinski_Space}:] is non empty set
product (Y --> Sierpinski_Space) is non empty strict TopSpace-like T_0 constituted-Functions TopStruct
(X,(product (Y --> Sierpinski_Space))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega (product (Y --> Sierpinski_Space)) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega (product (Y --> Sierpinski_Space)))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Y --> (X,Sierpinski_Space) is Relation-like Y -defined {(X,Sierpinski_Space)} -valued Function-like non empty V24(Y) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding Element of bool [:Y,{(X,Sierpinski_Space)}:]
{(X,Sierpinski_Space)} is non empty finite set
[:Y,{(X,Sierpinski_Space)}:] is non empty set
bool [:Y,{(X,Sierpinski_Space)}:] is non empty set
product (Y --> (X,Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,(product (Y --> Sierpinski_Space))) is non empty set
the carrier of (product (Y --> (X,Sierpinski_Space))) is functional non empty set
[: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):] is non empty set
the carrier of X is non empty set
the carrier of (product (Y --> Sierpinski_Space)) is non empty set
[: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):] is non empty set
bool [: the carrier of X, the carrier of (product (Y --> Sierpinski_Space)):] is non empty set
S is Relation-like the carrier of (X,(product (Y --> Sierpinski_Space))) -defined the carrier of (product (Y --> (X,Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (X,(product (Y --> Sierpinski_Space)))) quasi_total Element of bool [: the carrier of (X,(product (Y --> Sierpinski_Space))), the carrier of (product (Y --> (X,Sierpinski_Space))):]
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
S is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is 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
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is non empty set
F --> Sierpinski_Space is Relation-like F -defined {Sierpinski_Space} -valued Function-like non empty V24(F) quasi_total V384() non-Empty TopStruct-yielding Element of bool [:F,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty finite set
[:F,{Sierpinski_Space}:] is non empty set
bool [:F,{Sierpinski_Space}:] is non empty set
product (F --> Sierpinski_Space) is non empty strict TopSpace-like T_0 constituted-Functions TopStruct
F is Element of F
(F --> Sierpinski_Space) . F is non empty TopStruct
Y is non empty reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
F --> Y is Relation-like F -defined {Y} -valued Function-like non empty V24(F) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding Element of bool [:F,{Y}:]
{Y} is non empty finite set
[:F,{Y}:] is non empty set
bool [:F,{Y}:] is non empty set
W is Element of F
(F --> Y) . W is non empty reflexive transitive antisymmetric RelStr
product (F --> Y) is non empty constituted-Functions strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
F --> (X,Sierpinski_Space) is Relation-like F -defined {(X,Sierpinski_Space)} -valued Function-like non empty V24(F) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding Poset-yielding Element of bool [:F,{(X,Sierpinski_Space)}:]
{(X,Sierpinski_Space)} is non empty finite set
[:F,{(X,Sierpinski_Space)}:] is non empty set
bool [:F,{(X,Sierpinski_Space)}:] is non empty set
product (F --> (X,Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,(product (F --> Sierpinski_Space))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega (product (F --> Sierpinski_Space)) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega (product (F --> Sierpinski_Space)))) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
(X,F) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega F is 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
ContMaps (X,(Omega F)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the 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 BoolePoset 1 is 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 BoolePoset 1
InclPoset (bool 1) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of the 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 BoolePoset 1 is non empty set
the InternalRel of the 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 BoolePoset 1 is Relation-like the carrier of the 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 BoolePoset 1 -defined the carrier of the 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 BoolePoset 1 -valued Element of bool [: the carrier of the 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 BoolePoset 1, the carrier of the 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 BoolePoset 1:]
[: the carrier of the 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 BoolePoset 1, the carrier of the 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 BoolePoset 1:] is non empty set
bool [: the carrier of the 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 BoolePoset 1, the carrier of the 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 BoolePoset 1:] is non empty set
RelStr(# the carrier of the 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 BoolePoset 1, the InternalRel of the 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 BoolePoset 1 #) is strict RelStr
the carrier of (BoolePoset 1) is non empty set
the InternalRel of (BoolePoset 1) is Relation-like the carrier of (BoolePoset 1) -defined the carrier of (BoolePoset 1) -valued Element of bool [: the carrier of (BoolePoset 1), the carrier of (BoolePoset 1):]
[: the carrier of (BoolePoset 1), the carrier of (BoolePoset 1):] is non empty set
bool [: the carrier of (BoolePoset 1), the carrier of (BoolePoset 1):] is non empty set
RelStr(# the carrier of (BoolePoset 1), the InternalRel of (BoolePoset 1) #) is strict RelStr
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
Y is non empty non trivial TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete Scott TopRelStr
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of Y is non empty non trivial set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of bool [: the carrier of Y, the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopRelStr(# the carrier of Y, the InternalRel of Y, the topology of Y #) is strict TopRelStr
the carrier of (Omega Y) is non empty set
the InternalRel of (Omega Y) is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega Y) -valued Element of bool [: the carrier of (Omega Y), the carrier of (Omega Y):]
[: the carrier of (Omega Y), the carrier of (Omega Y):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega Y):] is non empty set
RelStr(# the carrier of (Omega Y), the InternalRel of (Omega Y) #) is strict RelStr
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
X is Relation-like Function-like set
disjoin X is Relation-like Function-like set
Union (disjoin X) is set
Y is set
X is Relation-like Function-like set
disjoin X is Relation-like Function-like set
Union (disjoin X) is Relation-like set
(Union (disjoin X)) ~ is Relation-like set
X is set
Y is set
[X,Y] is V33() set
{X,Y} is non empty finite set
{X} is non empty finite set
{{X,Y},{X}} is non empty finite V45() set
S is Relation-like Function-like set
(S) is Relation-like set
disjoin S is Relation-like Function-like set
Union (disjoin S) is Relation-like set
(Union (disjoin S)) ~ is Relation-like set
proj1 S is set
S . X is set
[Y,X] is V33() set
{Y,X} is non empty finite set
{Y} is non empty finite set
{{Y,X},{Y}} is non empty finite V45() set
[Y,X] `1 is set
[Y,X] `2 is set
X is finite set
proj1 X is set
proj2 X is set
Y is Relation-like Function-like set
proj1 Y is set
proj2 Y is set
S is set
F is set
[S,F] is V33() set
{S,F} is non empty finite set
{S} is non empty finite set
{{S,F},{S}} is non empty finite V45() set
[S,F] `1 is set
Y . [S,F] is set
S is Relation-like Function-like set
proj1 S is set
proj2 S is set
F is set
F is set
[F,F] is V33() set
{F,F} is non empty finite set
{F} is non empty finite set
{{F,F},{F}} is non empty finite V45() set
[F,F] `2 is set
S . [F,F] is set
Y is non empty TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
the carrier of Y is non empty set
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
InclPoset the topology of Y is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[:X,Y:] is non empty strict TopSpace-like TopStruct
the carrier of [:X,Y:] is non empty set
bool the carrier of [:X,Y:] is non empty set
S is 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
the carrier of S is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
F is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of S:]
(F) is Relation-like set
disjoin F is Relation-like Function-like set
Union (disjoin F) is Relation-like set
(Union (disjoin F)) ~ is Relation-like set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the carrier of (InclPoset the topology of Y) is non empty non trivial set
the InternalRel of (InclPoset the topology of Y) is Relation-like the carrier of (InclPoset the topology of Y) -defined the carrier of (InclPoset the topology of Y) -valued Element of bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):]
[: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) is strict RelStr
dom F is Element of bool the carrier of X
bool the carrier of X is non empty set
bool (bool the carrier of [:X,Y:]) is non empty set
F is Element of bool (bool the carrier of [:X,Y:])
union F is Element of bool the carrier of [:X,Y:]
bool the carrier of S is non empty set
W is Element of bool the carrier of S
y is set
F " W is Element of bool the carrier of X
W2 is set
F . y is set
[y,W2] is V33() set
{y,W2} is non empty finite set
{y} is non empty finite set
{{y,W2},{y}} is non empty finite V45() set
j is set
x is Element of bool the carrier of X
g1x is Element of bool the carrier of Y
[:x,g1x:] is Element of bool the carrier of [:X,Y:]
[x,g1x] is V33() set
{x,g1x} is non empty finite set
{x} is non empty finite set
{{x,g1x},{x}} is non empty finite V45() set
g2x is set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
a is set
[: the topology of X, the topology of Y:] is Relation-like bool the carrier of X -defined bool the carrier of Y -valued non empty Element of bool [:(bool the carrier of X),(bool the carrier of Y):]
[:(bool the carrier of X),(bool the carrier of Y):] is non empty set
bool [:(bool the carrier of X),(bool the carrier of Y):] is non empty set
a `1 is set
a `2 is set
[:(a `1),(a `2):] is set
W2 is Relation-like Function-like set
proj1 W2 is set
proj2 W2 is set
proj2 (proj2 W2) is set
bool (proj2 (proj2 W2)) is non empty set
{ (union b1) where b1 is Element of bool (proj2 (proj2 W2)) : b1 is finite } is set
x is set
g1x is Element of bool (proj2 (proj2 W2))
union g1x is set
{} (proj2 (proj2 W2)) is Function-like functional empty finite V45() Element of bool (proj2 (proj2 W2))
bool the carrier of (InclPoset the topology of Y) is non empty set
x is non empty Element of bool the carrier of (InclPoset the topology of Y)
g1x is Element of the carrier of (InclPoset the topology of Y)
g2x is Element of the carrier of (InclPoset the topology of Y)
a is Element of bool (proj2 (proj2 W2))
union a is set
b is Element of bool (proj2 (proj2 W2))
union b is set
a \/ b is Element of bool (proj2 (proj2 W2))
g1x "\/" g2x is Element of the carrier of (InclPoset the topology of Y)
hh is Element of the carrier of (InclPoset the topology of Y)
g1x \/ g2x is set
A is finite Element of bool (proj2 (proj2 W2))
union A is set
bool (F . y) is non empty Element of bool (bool (F . y))
bool (F . y) is non empty set
bool (bool (F . y)) is non empty set
g2x is set
a is set
[a,g2x] is V33() set
{a,g2x} is non empty finite set
{a} is non empty finite set
{{a,g2x},{a}} is non empty finite V45() set
[a,g2x] `1 is set
b is set
W2 . b is set
[a,g2x] `2 is set
[:a,g2x:] is set
b is set
W2 . b is set
b is set
[y,b] is V33() set
{y,b} is non empty finite set
{{y,b},{y}} is non empty finite V45() set
union x is set
W1 is Element of the carrier of X
F . W1 is Element of the carrier of S
g2x is set
a is set
b is Element of bool (proj2 (proj2 W2))
union b is set
bool (F . W1) is non empty Element of bool (bool (F . W1))
bool (F . W1) is non empty set
bool (bool (F . W1)) is non empty set
union (bool (F . W1)) is Element of bool (F . W1)
g2x is set
W2 . g2x is set
(W2 . g2x) `1 is set
(W2 . g2x) `2 is set
[((W2 . g2x) `1),((W2 . g2x) `2)] is V33() set
{((W2 . g2x) `1),((W2 . g2x) `2)} is non empty finite set
{((W2 . g2x) `1)} is non empty finite set
{{((W2 . g2x) `1),((W2 . g2x) `2)},{((W2 . g2x) `1)}} is non empty finite V45() set
{((W2 . g2x) `2)} is non empty finite set
a is Element of bool (proj2 (proj2 W2))
union a is set
"\/" (x,(InclPoset the topology of Y)) is Element of the carrier of (InclPoset the topology of Y)
g1x is non empty directed Element of bool the carrier of S
"\/" (g1x,S) is Element of the carrier of S
proj1 (proj2 W2) is set
a is set
b is Element of the carrier of S
A is Element of bool (proj2 (proj2 W2))
union A is set
hh is set
B is set
[B,hh] is V33() set
{B,hh} is non empty finite set
{B} is non empty finite set
{{B,hh},{B}} is non empty finite V45() set
B is set
W2 . B is set
B is set
g2x is open Element of bool the carrier of Y
[B,hh] `1 is set
[B,hh] `2 is set
[:B,hh:] is set
W2 . B is set
hh is Relation-like Function-like set
proj1 hh is set
proj2 hh is set
W2 .: (proj2 hh) is set
proj1 (W2 .: (proj2 hh)) is set
B is Element of bool (bool the carrier of X)
B is Element of bool (bool the carrier of X)
Intersect B is Element of bool the carrier of X
Q is Element of bool the carrier of X
Q is Element of bool the carrier of X
FinMeetCl the topology of X is Element of bool (bool the carrier of X)
c1 is set
c is Element of the carrier of X
F . c is Element of the carrier of S
p is set
q is set
hh . q is set
W2 . (hh . q) is set
q1 is set
[q1,q] is V33() set
{q1,q} is non empty finite set
{q1} is non empty finite set
{{q1,q},{q1}} is non empty finite V45() set
[:q1,q:] is set
[c,p] is V33() set
{c,p} is non empty finite set
{c} is non empty finite set
{{c,p},{c}} is non empty finite V45() set
c9 is Element of the carrier of (InclPoset the topology of Y)
b is Element of the carrier of (InclPoset the topology of Y)
c1 is set
c is set
[c1,c] is V33() set
{c1,c} is non empty finite set
{c1} is non empty finite set
{{c1,c},{c1}} is non empty finite V45() set
b is set
W2 . b is set
c9 is set
hh . c9 is set
W2 . (hh . c9) is set
p is set
[p,c9] is V33() set
{p,c9} is non empty finite set
{p} is non empty finite set
{{p,c9},{p}} is non empty finite V45() set
[:p,c9:] is set
W1 is Element of bool the carrier of X
[#] S is non empty non proper closed directed filtered lower upper Element of bool the carrier of S
Y is set
X is Relation-like set
S is Relation-like Function-like set
proj1 S is set
F is Relation-like Function-like set
proj1 F is set
F is set
S . F is set
Im (X,F) is set
{F} is non empty finite set
X .: {F} is set
F . F is set
X is Relation-like set
proj1 X is set
Y is set
(X,Y) is Relation-like Function-like set
((X,Y)) is Relation-like set
disjoin (X,Y) is Relation-like Function-like set
Union (disjoin (X,Y)) is Relation-like set
(Union (disjoin (X,Y))) ~ is Relation-like set
proj1 (X,Y) is set
S is set
F is set
[S,F] is V33() set
{S,F} is non empty finite set
{S} is non empty finite set
{{S,F},{S}} is non empty finite V45() set
(X,Y) . S is set
Im (X,S) is set
X .: {S} is set
F is set
[F,F] is V33() set
{F,F} is non empty finite set
{F} is non empty finite set
{{F,F},{F}} is non empty finite V45() set
X is TopSpace-like TopStruct
Y is TopSpace-like TopStruct
[:X,Y:] is strict TopSpace-like TopStruct
the carrier of [:X,Y:] is set
bool the carrier of [:X,Y:] is non empty set
S is Element of bool the carrier of [:X,Y:]
the carrier of X is set
the carrier of Y is set
[: the carrier of X, the carrier of Y:] is set
bool [: the carrier of X, the carrier of Y:] is non empty set
the topology of [:X,Y:] is non empty Element of bool (bool the carrier of [:X,Y:])
bool (bool the carrier of [:X,Y:]) is non empty set
S is Element of the topology of [:X,Y:]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
[:X,Y:] is non empty strict TopSpace-like TopStruct
the carrier of [:X,Y:] is non empty set
bool the carrier of [:X,Y:] is non empty set
the carrier of X is non empty set
the carrier of Y is non empty set
bool the carrier of Y is non empty set
S is Relation-like open Element of bool the carrier of [:X,Y:]
F is Element of the carrier of X
Im (S,F) is set
{F} is non empty finite set
S .: {F} is set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like the carrier of X -defined the carrier of Y -valued Element of bool [: the carrier of X, the carrier of Y:]
F .: {F} is Element of bool the carrier of Y
y is set
W is Element of bool the carrier of Y
W1 is set
[W1,y] is V33() set
{W1,y} is non empty finite set
{W1} is non empty finite set
{{W1,y},{W1}} is non empty finite V45() set
bool (bool the carrier of [:X,Y:]) is non empty set
bool the carrier of X is non empty set
W2 is Element of bool (bool the carrier of [:X,Y:])
union W2 is Relation-like Element of bool the carrier of [:X,Y:]
[F,y] is V33() set
{F,y} is non empty finite set
{{F,y},{F}} is non empty finite V45() set
j is set
x is Element of bool the carrier of X
g1x is Element of bool the carrier of Y
[:x,g1x:] is Relation-like Element of bool the carrier of [:X,Y:]
g2x is Element of bool the carrier of Y
a is set
[F,a] is V33() set
{F,a} is non empty finite set
{{F,a},{F}} is non empty finite V45() set
W1 is Element of bool the carrier of Y
Y is non empty TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
the carrier of Y is non empty set
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
InclPoset the topology of Y is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
X is non empty TopSpace-like TopStruct
[:X,Y:] is non empty strict TopSpace-like TopStruct
the carrier of [:X,Y:] is non empty set
bool the carrier of [:X,Y:] is non empty set
the carrier of X is non empty set
S is 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
the carrier of S is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
F is Relation-like open Element of bool the carrier of [:X,Y:]
(F, the carrier of X) is Relation-like Function-like set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
proj1 (F, the carrier of X) is set
the carrier of (InclPoset the topology of Y) is non empty non trivial set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the InternalRel of (InclPoset the topology of Y) is Relation-like the carrier of (InclPoset the topology of Y) -defined the carrier of (InclPoset the topology of Y) -valued Element of bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):]
[: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) is strict RelStr
proj2 (F, the carrier of X) is set
y is set
W1 is set
(F, the carrier of X) . W1 is set
W is Relation-like the carrier of X -defined the carrier of Y -valued Element of bool [: the carrier of X, the carrier of Y:]
W2 is Element of the carrier of X
Im (W,W2) is set
{W2} is non empty finite set
W .: {W2} is set
W is Relation-like the carrier of X -defined the carrier of Y -valued Element of bool [: the carrier of X, the carrier of Y:]
dom W is Element of bool the carrier of X
bool the carrier of X is non empty set
y is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of S:]
(y) is Relation-like set
disjoin y is Relation-like Function-like set
Union (disjoin y) is Relation-like set
(Union (disjoin y)) ~ is Relation-like set
Y is non empty TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
the carrier of Y is non empty set
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
InclPoset the topology of Y is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
X is non empty TopSpace-like TopStruct
[:X,Y:] is non empty strict TopSpace-like TopStruct
the carrier of [:X,Y:] is non empty set
bool the carrier of [:X,Y:] is non empty set
the carrier of X is non empty set
S is 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
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,S) is non empty set
F is Relation-like open Element of bool the carrier of [:X,Y:]
F is Relation-like open Element of bool the carrier of [:X,Y:]
(F, the carrier of X) is Relation-like Function-like set
(F, the carrier of X) is Relation-like Function-like set
W is Relation-like Function-like Element of the carrier of (X,S)
y is Relation-like Function-like Element of the carrier of (X,S)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the InternalRel of (Omega S) is Relation-like the carrier of (Omega S) -defined the carrier of (Omega S) -valued Element of bool [: the carrier of (Omega S), the carrier of (Omega S):]
[: the carrier of (Omega S), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega S), the carrier of (Omega S):] is non empty set
RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) is strict RelStr
the carrier of (InclPoset the topology of Y) is non empty non trivial set
the InternalRel of (InclPoset the topology of Y) is Relation-like the carrier of (InclPoset the topology of Y) -defined the carrier of (InclPoset the topology of Y) -valued Element of bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):]
[: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
bool [: the carrier of (InclPoset the topology of Y), the carrier of (InclPoset the topology of Y):] is non empty set
RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) is strict RelStr
j is set
W1 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
x is Element of the carrier of X
W1 . x is Element of the carrier of (Omega S)
W2 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 . x is Element of the carrier of (Omega S)
a is Element of the carrier of (Omega S)
W1 . j is set
b is Element of the carrier of (Omega S)
W2 . j is set
Im (F,x) is set
{x} is non empty finite set
F .: {x} is set
Im (F,x) is set
F .: {x} is set
g1x is Element of the carrier of (InclPoset the topology of Y)
g2x is Element of the carrier of (InclPoset the topology of Y)
Y is non empty TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
the carrier of Y is non empty set
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
InclPoset the topology of Y is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
X is non empty TopSpace-like TopStruct
[:X,Y:] is non empty strict TopSpace-like TopStruct
the topology of [:X,Y:] is non empty Element of bool (bool the carrier of [:X,Y:])
the carrier of [:X,Y:] is non empty set
bool the carrier of [:X,Y:] is non empty set
bool (bool the carrier of [:X,Y:]) is non empty set
InclPoset the topology of [:X,Y:] is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
the carrier of (InclPoset the topology of [:X,Y:]) is non empty non trivial set
the carrier of X is non empty set
S is 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
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,S) is non empty set
[: the carrier of (InclPoset the topology of [:X,Y:]), the carrier of (X,S):] is non empty set
bool [: the carrier of (InclPoset the topology of [:X,Y:]), the carrier of (X,S):] is non empty set
F is Relation-like the topology of [:X,Y:] -defined Function-like V24( the topology of [:X,Y:]) set
proj2 F is set
F is set
dom F is Element of bool the topology of [:X,Y:]
bool the topology of [:X,Y:] is non empty set
W is set
F . W is set
y is Relation-like Element of the topology of [:X,Y:]
(y, the carrier of X) is Relation-like Function-like set
the carrier of S is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
dom F is Element of bool the topology of [:X,Y:]
bool the topology of [:X,Y:] is non empty set
F is Relation-like the carrier of (InclPoset the topology of [:X,Y:]) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:X,Y:])) quasi_total Element of bool [: the carrier of (InclPoset the topology of [:X,Y:]), the carrier of (X,S):]
W is Element of the carrier of (InclPoset the topology of [:X,Y:])
y is Element of the carrier of (InclPoset the topology of [:X,Y:])
F . W is Relation-like Function-like Element of the carrier of (X,S)
F . y is Relation-like Function-like Element of the carrier of (X,S)
W1 is Relation-like open Element of bool the carrier of [:X,Y:]
W2 is Relation-like open Element of bool the carrier of [:X,Y:]
(W1, the carrier of X) is Relation-like Function-like set
(W2, the carrier of X) is Relation-like Function-like set
W is Relation-like open Element of bool the carrier of [:X,Y:]
F . W is set
(W, the carrier of X) is Relation-like Function-like set