:: WAYBEL26 semantic presentation

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

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() associative commutative L9()

1 is non empty set
{{},1} is non empty finite set
K722() is set
is non empty finite V45() set
K378() is M19()
is set
bool is non empty set
K39(K378(),) is set

{0,1} is non empty finite set
{1} is non empty finite set
{{},{1},{0,1}} is non empty finite set

the topology of Sierpinski_Space is non empty Element of bool ()
the carrier of Sierpinski_Space is non empty set
bool the carrier of Sierpinski_Space is non empty set
bool () 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

[: 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

X is set
X is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct

X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty strict RelStr

X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 TopStruct

X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct

the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
S is set
F is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct

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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) 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 ():] is non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct

the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] 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)
() |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (() |^ the carrier of X) is non empty set
F is Relation-like Function-like Element of the carrier of (() |^ the carrier of X)
W is Relation-like Function-like Element of the carrier of (() |^ the carrier of X)
y is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
W1 is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
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 (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 () is non empty set
bool the carrier of () is non empty set
() |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (() |^ the carrier of X) is non empty set
bool the carrier of (() |^ the carrier of X) is non empty set
W is Element of bool the carrier of (() |^ the carrier of X)
pi (W,S) is Element of bool the carrier of ()
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct

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
() |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (() |^ the carrier of X) is non empty set
bool the carrier of (() |^ the carrier of X) is non empty set
W is non empty Element of bool the carrier of (() |^ the carrier of X)
pi (W,S) 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 [::]
[::] is non empty set
bool [::] is non empty set

the carrier of () 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 () is non empty set

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

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
[: the carrier of X,{{},1}:] is non empty set
bool [: the carrier of X,{{},1}:] is non empty 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 is non empty set
[: the carrier of X, the carrier of :] is non empty set
bool [: the carrier of X, the carrier of :] is non empty set
x is Relation-like the carrier of X -defined the carrier of -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of :]
g1x is Relation-like the carrier of X -defined the carrier of -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of :]
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

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

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 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)

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:]

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

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
[: 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)

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:]

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

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
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

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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) 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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
W1 is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of ():]
y is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total continuous monotone Element of bool [: the carrier of (), the carrier of ():]
y * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of () -valued the carrier of () -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 ():]
W2 is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of ():]
y * W2 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of () -valued the carrier of () -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 ():]
[: 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 ()
W2 . a is Element of the carrier of ()
y . (W2 . a) is Element of the carrier of ()
W1 . a is Element of the carrier of ()
(y * W1) . a is Element of the carrier of ()
y . (W1 . a) is Element of the carrier of ()
b is Element of the carrier of ()
A is Element of the carrier of ()
(y * W1) . g2x is set
(y * W2) . g2x is set
x is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
g1x is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
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):]

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

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 () is non empty set
[: the carrier of S, the carrier of ():] is non empty set
bool [: the carrier of S, the carrier of ():] 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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) 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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
W1 is Relation-like the carrier of S -defined the carrier of () -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of ():]
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 () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total continuous monotone Element of bool [: the carrier of (), the carrier of ():]

y is Relation-like the carrier of S -defined the carrier of () -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of ():]

[: the carrier of Y, the carrier of ():] is non empty set
bool [: the carrier of Y, the carrier of ():] 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 () -valued the carrier of () -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 ():]
a is Element of the carrier of Y
(y * F) . a is Element of the carrier of ()
F . a is Element of the carrier of S
y . (F . a) is Element of the carrier of ()
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of () -valued the carrier of () -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 ():]
(W1 * F) . a is Element of the carrier of ()
W1 . (F . a) is Element of the carrier of ()
(y * F) . g2x is set
(W1 * F) . g2x is set
x is Relation-like the carrier of Y -defined the carrier of () -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of ():]
g1x is Relation-like the carrier of Y -defined the carrier of () -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of ():]
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):]

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

the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set

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 ()
the carrier of () is non empty set
bool the carrier of () is non empty set
(X,Y,W,y) is Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () 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 . 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 . 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

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
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 () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] 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)

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)

g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of () |^ the carrier of X
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of (() |^ the carrier of X) is non empty set
bool the carrier of (() |^ the carrier of X) is non empty set
a is non empty directed Element of bool the carrier of g2x

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 (() |^ the carrier of X) is non empty set
bool the carrier of (() |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of X --> () is Relation-like the carrier of X -defined {()} -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,{()}:]
{()} is non empty finite set
[: the carrier of X,{()}:] is non empty set
bool [: the carrier of X,{()}:] is non empty set
the carrier of X --> () is Relation-like the carrier of X -defined {()} -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,{()}:]
{()} is non empty finite set
[: the carrier of X,{()}:] is non empty set
bool [: 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 () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) 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 () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
hh is non empty directed Element of bool the carrier of (() |^ the carrier of X)
"\/" (hh,(() |^ the carrier of X)) is Relation-like Function-like Element of the carrier of (() |^ the carrier of X)
product ( the carrier of X --> ()) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> ())) is functional non empty set
bool the carrier of (product ( the carrier of X --> ())) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> ()) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> ()) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> ()))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> ()) . c1)
the carrier of (( the carrier of X --> ()) . c1) is non empty set
bool the carrier of (( the carrier of X --> ()) . c1) is non empty set
product ( the carrier of X --> ()) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> ())) is functional non empty set
bool the carrier of (product ( the carrier of X --> ())) is non empty set
b is non empty directed Element of bool the carrier of (() |^ the carrier of X)
"\/" (b,(() |^ the carrier of X)) is Relation-like Function-like Element of the carrier of (() |^ the carrier of X)
c is Element of the carrier of X
( the carrier of X --> ()) . 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 --> ()))
pi (c1,c) is non empty Element of bool the carrier of (( the carrier of X --> ()) . c)
( the carrier of X --> ()) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> ()) . c) is non empty set
bool the carrier of (( the carrier of X --> ()) . c) is non empty set
( the carrier of X --> ()) . c is non empty reflexive transitive antisymmetric RelStr
b is non empty directed Element of bool the carrier of ()
"\/" (c1,(product ( the carrier of X --> ()))) is Relation-like Function-like Element of the carrier of (product ( the carrier of X --> ()))
("\/" (c1,(product ( the carrier of X --> ())))) . c is Element of the carrier of (( the carrier of X --> ()) . c)
"\/" ((pi (c1,c)),(( the carrier of X --> ()) . c)) is Element of the carrier of (( the carrier of X --> ()) . c)
Q is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of (), the carrier of ():]
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> ()) . c)
( the carrier of X --> ()) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> ()) . c) is non empty set
bool the carrier of (( the carrier of X --> ()) . c) is non empty set
Q .: b is non empty Element of bool the carrier of ()
W1 is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
W1 . c is Element of the carrier of ()
"\/" ((pi (Q,c)),(( the carrier of X --> ()) . c)) is Element of the carrier of (( the carrier of X --> ()) . c)
"\/" (b,()) is Element of the carrier of ()
F . ("\/" (b,())) 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 () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
W2 . c is Element of the carrier of ()
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 (S,X) is non empty set
bool the carrier of (S,X) is non empty set

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 ()
the carrier of () is non empty set
bool the carrier of () is non empty set
(S,X,(F . W),y) is Element of bool the carrier of ()
W1 is 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 . (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

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 () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
bool [: the carrier of X, the carrier of ():] 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)

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)

g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of () |^ the carrier of Y
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of (() |^ the carrier of Y) is non empty set
bool the carrier of (() |^ the carrier of Y) is non empty set
a is non empty directed Element of bool the carrier of g2x

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 (() |^ the carrier of X) is non empty set
bool the carrier of (() |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of Y --> () is Relation-like the carrier of Y -defined {()} -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,{()}:]
{()} is non empty finite set
[: the carrier of Y,{()}:] is non empty set
bool [: the carrier of Y,{()}:] is non empty set
the carrier of X --> () is Relation-like the carrier of X -defined {()} -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,{()}:]
[: the carrier of X,{()}:] is non empty set
bool [: the carrier of X,{()}:] is non empty set
hh is non empty directed Element of bool the carrier of (() |^ the carrier of X)
"\/" (hh,(() |^ the carrier of X)) is Relation-like Function-like Element of the carrier of (() |^ the carrier of X)
product ( the carrier of X --> ()) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> ())) is functional non empty set
bool the carrier of (product ( the carrier of X --> ())) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> ()) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> ()) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> ()))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> ()) . c1)
the carrier of (( the carrier of X --> ()) . c1) is non empty set
bool the carrier of (( the carrier of X --> ()) . c1) is non empty set
product ( the carrier of Y --> ()) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of Y --> ())) is functional non empty set
bool the carrier of (product ( the carrier of Y --> ())) is non empty set
b is non empty directed Element of bool the carrier of (() |^ the carrier of Y)
"\/" (b,(() |^ the carrier of Y)) is Relation-like Function-like Element of the carrier of (() |^ 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 --> ()) . (F . c) is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> ()) . c is non empty reflexive transitive antisymmetric RelStr
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> ()) . c)
( the carrier of X --> ()) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> ()) . c) is non empty set
bool the carrier of (( the carrier of X --> ()) . c) is non empty set
c1 is functional non empty directed Element of bool the carrier of (product ( the carrier of Y --> ()))
pi (c1,(F . c)) is non empty Element of bool the carrier of (( the carrier of Y --> ()) . (F . c))
( the carrier of Y --> ()) . (F . c) is non empty reflexive RelStr
the carrier of (( the carrier of Y --> ()) . (F . c)) is non empty set
bool the carrier of (( the carrier of Y --> ()) . (F . c)) is non empty set
W1 is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
W1 . c is Element of the carrier of ()
"\/" ((pi (Q,c)),(( the carrier of X --> ()) . c)) is Element of the carrier of (( the carrier of X --> ()) . c)
"\/" (c1,(product ( the carrier of Y --> ()))) is Relation-like Function-like Element of the carrier of (product ( the carrier of Y --> ()))
("\/" (c1,(product ( the carrier of Y --> ())))) . (F . c) is Element of the carrier of (( the carrier of Y --> ()) . (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 () -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of ():]
W2 . c is Element of the carrier of ()
Y is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct

S is non empty TopSpace-like SubSpace of Y

[#] 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