:: WAYBEL25 semantic presentation

K176() is Element of bool K172()
K172() is set
bool K172() is non empty set
K122() is set
bool K122() is non empty set

1 is non empty set
{{},1} is non empty set
bool K176() is non empty set

the carrier of I[01] is non empty set
K173() is set
K174() is set
K175() is set
[:K172(),K172():] is Relation-like set
bool [:K172(),K172():] is non empty set
K491() is non empty V147() L11()
the carrier of K491() is non empty set
K496() is non empty L11()
K497() is non empty V147() M32(K496())
K498() is non empty V147() V169() V229() M35(K496(),K497())
K500() is non empty V147() V169() V171() V173() L11()
K501() is non empty V147() V169() V229() M32(K500())
K726() is set

K462() is M29()

bool is non empty set
K39(K462(),) is set

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

K256(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 is non empty set
Y is Element of the carrier of Sierpinski_Space
{Y} is non empty compact Element of bool the carrier of Sierpinski_Space
bool the carrier of Sierpinski_Space is non empty set

L is set
L is set
the topology of Sierpinski_Space is non empty Element of bool ()
bool () is non empty set
Y is Element of the carrier of Sierpinski_Space
{Y} is non empty compact Element of bool the carrier of Sierpinski_Space
bool the carrier of Sierpinski_Space is non empty set

L is set
L is set
the topology of Sierpinski_Space is non empty Element of bool ()
bool () is non empty set
Y is Element of the carrier of Sierpinski_Space
{Y} is non empty compact Element of bool the carrier of Sierpinski_Space
bool the carrier of Sierpinski_Space is non empty set

Y is Element of the carrier of Sierpinski_Space
{Y} is non empty compact Element of bool the carrier of Sierpinski_Space
bool the carrier of Sierpinski_Space is non empty set

L is non empty set

{()} is non empty set
[:L,{()}:] is Relation-like non empty set
bool [:L,{()}:] is non empty set

is non empty set

bool is non empty set

the carrier of () is non empty set

the carrier of C is non empty set
Carrier (L --> ()) is Relation-like L -defined Function-like V24(L) set
dom (Carrier (L --> ())) is Element of bool L
bool L is non empty set

dom () is Element of bool L
D is set
(Carrier (L --> ())) . D is set
() . D is set
() . D is set
(L --> ()) . D is set
the carrier of () is non empty set
D is 1-sorted
the carrier of D is set
D is 1-sorted
the carrier of D is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
RelStr(# the carrier of C, the InternalRel of C #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the carrier of (product (L --> ())) is non empty set
the InternalRel of (product (L --> ())) is Relation-like the carrier of (product (L --> ())) -defined the carrier of (product (L --> ())) -valued Element of bool [: the carrier of (product (L --> ())), the carrier of (product (L --> ())):]
[: the carrier of (product (L --> ())), the carrier of (product (L --> ())):] is Relation-like non empty set
bool [: the carrier of (product (L --> ())), the carrier of (product (L --> ())):] is non empty set
RelStr(# the carrier of (product (L --> ())), the InternalRel of (product (L --> ())) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
product (Carrier (L --> ())) is set
product () is 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 Relation-like non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set

the carrier of L is non empty set

the carrier of C is non empty set
[: the carrier of L, the carrier of C:] is Relation-like non empty set
bool [: the carrier of L, the carrier of C:] is non empty set
D 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:]
D is Relation-like the carrier of L -defined the carrier of C -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of C:]
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 Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
RelStr(# the carrier of C, the InternalRel of C #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
[: the carrier of C, the carrier of L:] is Relation-like non empty set
bool [: the carrier of C, the carrier of L:] is non empty set
D " is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
V is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of X:]

rng D is non empty Element of bool the carrier of C
bool the carrier of C is non empty set

N is Relation-like the carrier of C -defined the carrier of L -valued Function-like non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of L:]
dom N is non empty Element of bool the carrier of C
D " is Relation-like the carrier of C -defined the carrier of L -valued Function-like non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of L:]
M is set
N . M is set
(D ") . M is set
(D ") . M is set
M is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total monotone sups-preserving join-preserving directed-sups-preserving Element of bool [: the carrier of Y, the carrier of X:]
dom (D ") is non empty Element of bool the carrier of C
M is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total monotone sups-preserving join-preserving directed-sups-preserving Element of bool [: the carrier of X, the carrier of Y:]
dom D is non empty Element of bool the carrier of L
bool the carrier of L 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 Relation-like non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
D 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:]
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 Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the carrier of C is non empty set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
RelStr(# the carrier of C, the InternalRel of C #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
[: the carrier of L, the carrier of C:] is Relation-like non empty set
bool [: the carrier of L, the carrier of C:] is non empty set
D is Relation-like the carrier of L -defined the carrier of C -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of C:]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
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 Relation-like non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
L 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:]
C is non empty TopSpace-like TopStruct
the carrier of C is non empty set
[: the carrier of C, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of C, the carrier of Y:] is non empty set
D is Relation-like the carrier of C -defined the carrier of Y -valued Function-like non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of Y:]
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
[: the carrier of D, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of D, the carrier of Y:] is non empty set
[#] C is non empty non proper open closed dense non boundary Element of bool the carrier of C
bool the carrier of C is non empty set
[#] D is non empty non proper open closed dense non boundary Element of bool the carrier of D
bool the carrier of D is non empty set
L " is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
(L ") * D is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of X:]
[: the carrier of C, the carrier of X:] is Relation-like non empty set
bool [: the carrier of C, the carrier of X:] is non empty set
[: the carrier of D, the carrier of X:] is Relation-like non empty set
bool [: the carrier of D, the carrier of X:] is non empty set
V is Relation-like the carrier of D -defined the carrier of X -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of X:]
V | the carrier of C is Relation-like the carrier of C -defined the carrier of D -defined the carrier of X -valued Function-like Element of bool [: the carrier of D, the carrier of X:]
L * V is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
M is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
M | the carrier of C is Relation-like the carrier of C -defined the carrier of D -defined the carrier of Y -valued Function-like Element of bool [: the carrier of D, the carrier of Y:]
rng L is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
dom D is non empty Element of bool the carrier of C
M is set
M . M is set
D . M is set
rng D is non empty Element of bool the carrier of Y
dom (L ") is non empty Element of bool the carrier of Y
dom V is non empty Element of bool the carrier of D
V . M is set
L . (V . M) is set
((L ") * D) . M is set
L . (((L ") * D) . M) is set
(L ") . (D . M) is set
L . ((L ") . (D . M)) is set
L * (L ") is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
(L * (L ")) . (D . M) is set
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) . (D . M) is set
the carrier of D /\ the carrier of C is set
dom M is non empty Element of bool the carrier of D
(dom M) /\ the carrier of C is Element of bool the carrier of D

X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
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 Relation-like non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
[: the carrier of Y, the carrier of X:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
id 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 open Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
L is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
L * L is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
Image L is non empty TopSpace-like SubSpace of Y
rng L is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
Y | (rng L) is non empty strict TopSpace-like SubSpace of Y
the carrier of () is non empty set
[: the carrier of (), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (), the carrier of X:] is non empty set
C is Relation-like the carrier of () -defined the carrier of X -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of X:]
corestr L is Relation-like the carrier of Y -defined the carrier of () -valued Function-like non empty V24( the carrier of Y) quasi_total onto Element of bool [: the carrier of Y, the carrier of ():]
[: the carrier of Y, the carrier of ():] is Relation-like non empty set
bool [: the carrier of Y, the carrier of ():] is non empty set
C " 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 ():]
[: the carrier of X, the carrier of ():] is Relation-like non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
incl () is Relation-like the carrier of () -defined the carrier of Y -valued Function-like non empty V24( the carrier of ()) quasi_total continuous Element of bool [: the carrier of (), the carrier of Y:]
[: the carrier of (), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (), the carrier of Y:] is non empty set
(incl ()) * (C ") 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:]
C * () is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of X:]
D 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:]
D 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:]
D * D 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:]
rng C is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
() * ((incl ()) * (C ")) 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 ():]
C * (() * ((incl ()) * (C "))) 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:]
() * (incl ()) is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
(() * (incl ())) * (C ") 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 ():]
C * ((() * (incl ())) * (C ")) 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:]
id () is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total continuous open Element of bool [: the carrier of (), the carrier of ():]
id the carrier of () is Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
(id ()) * (C ") 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 ():]
C * ((id ()) * (C ")) 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:]
C * (C ") 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:]
L 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:]
C 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:]
C * L 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:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
L * C 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:]
D 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:]
D * D 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:]
Image D is non empty TopSpace-like SubSpace of Y
rng D is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
Y | (rng D) is non empty strict TopSpace-like SubSpace of Y
dom L is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
rng C is non empty Element of bool the carrier of X
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is Relation-like non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
corestr L is Relation-like the carrier of X -defined the carrier of () -valued Function-like non empty V24( the carrier of X) quasi_total onto Element of bool [: the carrier of X, the carrier of ():]
Image L is non empty TopSpace-like SubSpace of Y
rng L is non empty Element of bool the carrier of Y
Y | (rng L) is non empty strict TopSpace-like SubSpace of Y
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is Relation-like non empty set
bool [: the carrier of X, the carrier of ():] is non empty set
id () is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total continuous open Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
id the carrier of () is Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (), the carrier of Y:] is non empty set
[: the carrier of (), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (), the carrier of X:] is non empty set
C * (id ()) is Relation-like the carrier of () -defined the carrier of X -valued Function-like Element of bool [: the carrier of (), the carrier of X:]
[: the carrier of (), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (), the carrier of X:] is non empty set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
N is Relation-like the carrier of () -defined the carrier of X -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of X:]
V is Element of bool the carrier of X
N " V is Element of bool the carrier of ()
bool the carrier of () is non empty set
dom (id ()) is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()
C " V is Element of bool the carrier of Y
(id ()) " (C " V) is Element of bool the carrier of ()
(C " V) /\ ([#] ()) is Element of bool the carrier of ()
M is set
(id ()) . M is set
M is set
(id ()) . M is set
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
the topology of () is non empty Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
D 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 ():]
D " is Relation-like the carrier of () -defined the carrier of X -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of X:]
D * (D ") is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
C * (D * (D ")) is Relation-like the carrier of () -defined the carrier of X -valued Function-like Element of bool [: the carrier of (), the carrier of X:]
(id X) * (D ") is Relation-like the carrier of () -defined the carrier of X -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of X:]
C * (L * C) 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:]
L * (C * (L * C)) 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:]
(id X) * C 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:]
L * ((id X) * C) 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:]
V is Relation-like the carrier of () -defined the carrier of X -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of X:]
dom V is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()
rng V is non empty Element of bool the carrier of X
V " 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 ():]
rng () is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()

C * (id the carrier of ()) is Relation-like the carrier of () -defined the carrier of X -valued Function-like Element of bool [: the carrier of (), the carrier of X:]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
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
Y is non empty 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
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
C is non empty TopSpace-like TopStruct
the carrier of C is non empty set
the topology of C is non empty Element of bool (bool the carrier of C)
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
TopStruct(# the carrier of C, the topology of C #) is non empty strict TopSpace-like TopStruct
[: the carrier of X, the carrier of L:] is Relation-like non empty set
bool [: the carrier of X, the carrier of L:] is non empty set
[: the carrier of L, the carrier of X:] is Relation-like non empty set
bool [: the carrier of L, the carrier of X:] is non empty set
id 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 open Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
D is Relation-like the carrier of X -defined the carrier of L -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of L:]
D is Relation-like the carrier of L -defined the carrier of X -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of X:]
D * D 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:]
[: the carrier of C, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of C, the carrier of Y:] is non empty set
[: the carrier of Y, the carrier of C:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of C:] is non empty set
V is Relation-like the carrier of Y -defined the carrier of C -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of C:]
id Y 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 open Element of bool [: the carrier of Y, the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
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:]
N is Relation-like the carrier of C -defined the carrier of Y -valued Function-like non empty V24( the carrier of C) quasi_total continuous Element of bool [: the carrier of C, the carrier of Y:]
N * V 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:]
Y is non empty TopStruct
L is non empty TopStruct
X is non empty TopStruct
the carrier of Y is non empty set
the carrier of L is non empty set
[: the carrier of Y, the carrier of L:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of L:] is non empty set
C is Relation-like the carrier of Y -defined the carrier of L -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of L:]
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
D 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:]
D * D 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:]
Image D is non empty SubSpace of X
rng D is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
X | (rng D) is non empty strict SubSpace of X
the carrier of () is non empty set
[: the carrier of (), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (), the carrier of Y:] is non empty set
D is Relation-like the carrier of () -defined the carrier of Y -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of Y:]
C * D is Relation-like the carrier of () -defined the carrier of L -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of L:]
[: the carrier of (), the carrier of L:] is Relation-like non empty set
bool [: the carrier of (), the carrier of L:] is non empty set
Y is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
L is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
L * L is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
Image L is non empty TopSpace-like SubSpace of Y
rng L is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
Y | (rng L) is non empty strict TopSpace-like SubSpace of Y
corestr L is Relation-like the carrier of Y -defined the carrier of () -valued Function-like non empty V24( the carrier of Y) quasi_total onto Element of bool [: the carrier of Y, the carrier of ():]
the carrier of () is non empty set
[: the carrier of Y, the carrier of ():] is Relation-like non empty set
bool [: the carrier of Y, the carrier of ():] is non empty set
D is Element of the carrier of Y
() . D is Element of the carrier of ()
dom L is non empty Element of bool the carrier of Y
D is set
L . D is set
X is non empty TopSpace-like injective TopStruct
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
the carrier of X is non empty set
[: the carrier of Y, the carrier of X:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
id 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 open Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
L is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of X:]
L | the carrier of X is Relation-like the carrier of Y -defined the carrier of X -defined the carrier of Y -defined the carrier of X -valued Function-like Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
bool the carrier of Y is non empty set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
bool the carrier of X is non empty set
C is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
C * C is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
Image C is non empty TopSpace-like SubSpace of Y
rng C is non empty Element of bool the carrier of Y
Y | (rng C) is non empty strict TopSpace-like SubSpace of Y
dom L is non empty Element of bool the carrier of Y
L * L is Relation-like the carrier of Y -defined the carrier of X -valued Function-like Element of bool [: the carrier of Y, the carrier of X:]
D is set
(L * L) . D is set
L . D is set
L . (L . D) is set
(id X) . (L . D) is set
dom (C * C) is non empty Element of bool the carrier of Y
rng L is non empty Element of bool the carrier of X
D is set
L . D is set
(L | the carrier of X) . D is set
D is non empty Element of bool the carrier of Y
Y | D is non empty strict TopSpace-like SubSpace of Y
the carrier of (Y | D) is non empty set
[#] (Y | D) is non empty non proper open closed dense non boundary Element of bool the carrier of (Y | D)
bool the carrier of (Y | D) is non empty 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
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
D is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
D * D is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of Y:]
Image D is non empty TopSpace-like SubSpace of Y
rng D is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
Y | (rng D) is non empty strict TopSpace-like SubSpace of Y

L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
the carrier of Y is non empty set
[: the carrier of L, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of L, the carrier of Y:] is non empty set
C is Relation-like the carrier of L -defined the carrier of Y -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of Y:]
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
[: the carrier of D, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of D, the carrier of Y:] is non empty set
bool the carrier of D is non empty set
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : a1 in b1 } is set
"\/" ( { (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : a1 in b1 } ,Y) is Element of the carrier of Y
D is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
N is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
N | the carrier of L is Relation-like the carrier of L -defined the carrier of D -defined the carrier of Y -valued Function-like Element of bool [: the carrier of D, the carrier of Y:]
dom C is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
bool the carrier of Y is non empty set
V is Element of bool the carrier of Y
N " V is Element of bool the carrier of D

N " M is Element of bool the carrier of D
M is set
M is Element of the carrier of D
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } is set
A is set
i is open Element of bool the carrier of D
i /\ the carrier of L is Element of bool the carrier of D
C .: (i /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (i /\ the carrier of L)) is Element of the carrier of Y
[#] D is non empty non proper open closed dense non boundary Element of bool the carrier of D
([#] D) /\ the carrier of L is Element of bool the carrier of D
C .: (([#] D) /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (([#] D) /\ the carrier of L)) is Element of the carrier of Y
A is Element of bool the carrier of Y
i is Element of the carrier of Y
g is Element of the carrier of Y
g9 is open Element of bool the carrier of D
g9 /\ the carrier of L is Element of bool the carrier of D
C .: (g9 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g9 /\ the carrier of L)) is Element of the carrier of Y
g99 is open Element of bool the carrier of D
g99 /\ the carrier of L is Element of bool the carrier of D
C .: (g99 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g99 /\ the carrier of L)) is Element of the carrier of Y
g9 /\ g99 is open Element of bool the carrier of D
(g9 /\ g99) /\ the carrier of L is Element of bool the carrier of D
C .: ((g9 /\ g99) /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: ((g9 /\ g99) /\ the carrier of L)) is Element of the carrier of Y
N . M is Element of the carrier of Y
"\/" (A,Y) is Element of the carrier of Y
i is set
g is open Element of bool the carrier of D
g /\ the carrier of L is Element of bool the carrier of D
C .: (g /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g /\ the carrier of L)) is Element of the carrier of Y
g99 is set
t9 is Element of the carrier of D
N . t9 is Element of the carrier of Y
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : t9 in b1 } is set
"\/" ( { (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : t9 in b1 } ,Y) is Element of the carrier of Y
g9 is Element of the carrier of Y
M is Element of bool the carrier of D
M is set
(N | the carrier of L) . M is set
C . M is set
M is Element of the carrier of L
M is Element of the carrier of D
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } is set
A is set
i is open Element of bool the carrier of D
i /\ the carrier of L is Element of bool the carrier of D
C .: (i /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (i /\ the carrier of L)) is Element of the carrier of Y
A is Element of bool the carrier of Y
C . M is Element of the carrier of Y
i is Element of the carrier of Y
g is open Element of bool the carrier of D
g /\ the carrier of L is Element of bool the carrier of D
C .: (g /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g /\ the carrier of L)) is Element of the carrier of Y
i is Element of the carrier of Y
g is open Element of bool the carrier of L
C .: g is Element of bool the carrier of Y
inf (C .: g) is Element of the carrier of Y
the topology of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
the topology of D is non empty Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
[#] L is non empty non proper open closed dense non boundary Element of bool the carrier of L
g9 is Element of bool the carrier of D
g9 /\ ([#] L) is Element of bool the carrier of L
g99 is open Element of bool the carrier of D
g99 /\ the carrier of L is Element of bool the carrier of D
C .: (g99 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g99 /\ the carrier of L)) is Element of the carrier of Y
waybelow (C . M) is non empty directed lower Element of bool the carrier of Y
g is Element of the carrier of Y
wayabove g is upper Element of bool the carrier of Y
C " () is Element of bool the carrier of L
C .: (C " ()) is Element of bool the carrier of Y
inf () is Element of the carrier of Y
inf (C .: (C " ())) is Element of the carrier of Y

"\/" ((waybelow (C . M)),Y) is Element of the carrier of Y
N . M is Element of the carrier of Y
"\/" ( { (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } ,Y) is Element of the carrier of Y

dom (N | the carrier of L) is Element of bool the carrier of L
dom N is non empty Element of bool the carrier of D
(dom N) /\ the carrier of L is Element of bool the carrier of D
the carrier of D /\ the carrier of L is set

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

the carrier of L is set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is strict TopStruct
C is Element of the carrier of L
D is Element of the carrier of L
{D} is non empty set
[C,D] is set
{C,D} is non empty set
{C} is non empty set
{{C,D},{C}} is non empty set
D is Element of bool the carrier of X
Cl D is Element of bool the carrier of X

the carrier of Y is set
the topology of Y is 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 strict TopStruct

the carrier of L is set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is strict TopStruct
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 Relation-like set
bool [: the carrier of Y, the carrier of Y:] is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
C is set
D is set
[C,D] is set
{C,D} is non empty set
{C} is non empty set
{{C,D},{C}} is non empty set
D is Element of the carrier of Y
N is Element of the carrier of Y
{N} is non empty set
V is Element of the carrier of L
M is Element of the carrier of L
M is Element of bool the carrier of X
Cl M is Element of bool the carrier of X
D is Element of the carrier of L
N is Element of the carrier of L
{N} is non empty set
V is Element of the carrier of Y
M is Element of the carrier of Y
M is Element of bool the carrier of X
Cl M is Element of bool the carrier of X
X is TopStruct
the carrier of X is set
(X) is strict TopRelStr
the carrier of (X) is set
the topology of X is 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 strict TopStruct
the topology of (X) is 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 strict TopStruct

(X) is strict TopRelStr
the carrier of (X) is set

X is non empty TopStruct
(X) is strict TopRelStr
the carrier of (X) is set
the carrier of X is non empty set

(X) is strict TopRelStr
the carrier of (X) is set
the topology of (X) is 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 strict TopStruct
the carrier of X is set
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 strict TopSpace-like TopStruct
Y is Element of bool (bool the carrier of (X))
K252( the carrier of (X),Y) is Element of bool the carrier of (X)
L is Element of bool the carrier of (X)
C is Element of bool the carrier of (X)
L /\ C is Element of bool the carrier of (X)
X is TopStruct
(X) is strict TopRelStr
Y is set
the carrier of (X) is set
[Y,Y] is set
{Y,Y} is non empty set
{Y} is non empty set
{{Y,Y},{Y}} is non empty set
the InternalRel of (X) is Relation-like the carrier of (X) -defined the carrier of (X) -valued Element of bool [: the carrier of (X), the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is Relation-like set
bool [: the carrier of (X), the carrier of (X):] is non empty set
L is non empty TopStruct
the carrier of L is non empty set
the carrier of X is set
bool the carrier of X is non empty set
D is Element of the carrier of L
{D} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
D is Element of bool the carrier of X
Cl D is Element of bool the carrier of X
C is Element of the carrier of (X)
X is TopStruct
the carrier of X is set
bool the carrier of X is non empty set
Y is Element of the carrier of X
{Y} is non empty set
L is Element of the carrier of X
{L} is non empty set
C is Element of bool the carrier of X
D is Element of bool the carrier of X
Cl D is Element of bool the carrier of X
Cl C is Element of bool the carrier of X
D is Element of bool the carrier of X
X is TopStruct
(X) is reflexive strict TopRelStr
Y is set
the carrier of (X) is set
L is set
C is set
[Y,L] is set
{Y,L} is non empty set
{Y} is non empty set
{{Y,L},{Y}} is non empty set
the InternalRel of (X) is Relation-like the carrier of (X) -defined the carrier of (X) -valued Element of bool [: the carrier of (X), the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is Relation-like set
bool [: the carrier of (X), the carrier of (X):] is non empty set
[L,C] is set
{L,C} is non empty set
{L} is non empty set
{{L,C},{L}} is non empty set
[Y,C] is set
{Y,C} is non empty set
{{Y,C},{Y}} is non empty set
D is Element of the carrier of (X)
D is Element of the carrier of (X)
the carrier of X is set
bool the carrier of X is non empty set
{D} is non empty set
V is Element of bool the carrier of X
Cl V is Element of bool the carrier of X
the topology of (X) is 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 strict TopStruct
the topology of X is 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 strict TopStruct
N is Element of the carrier of (X)
{N} is non empty set
M is Element of bool the carrier of X
Cl M is Element of bool the carrier of X
M is Element of the carrier of X
{M} is non empty set
X is non empty TopSpace-like T_0 TopStruct

Y is set
the carrier of (X) is non empty set
L is set
[Y,L] is set
{Y,L} is non empty set
{Y} is non empty set
{{Y,L},{Y}} is non empty set
the InternalRel of (X) is Relation-like the carrier of (X) -defined the carrier of (X) -valued Element of bool [: the carrier of (X), the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier of (X), the carrier of (X):] is non empty set
[L,Y] is set
{L,Y} is non empty set
{L} is non empty set
{{L,Y},{L}} is non empty set
D is Element of the carrier of (X)
C is Element of the carrier of (X)
the carrier of X is non empty set
bool the carrier of X is non empty set
{C} is non empty compact Element of bool the carrier of (X)
bool the carrier of (X) is non empty 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
TopStruct(# the carrier of (X), the topology of (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
{D} is non empty compact Element of bool the carrier of (X)
D is Element of the carrier of X
N is Element of the carrier of X
V is Element of bool the carrier of X
M is Element of bool the carrier of X
Cl M is closed Element of bool the carrier of X
M is Element of bool the carrier of X
Cl M is closed Element of bool the carrier of X

the carrier of X is set
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 strict TopSpace-like TopStruct

the carrier of Y is 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 strict TopSpace-like TopStruct

the carrier of (X) is set
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 strict TopSpace-like TopStruct
the carrier of (Y) is 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 strict TopSpace-like TopStruct
the InternalRel of (X) is Relation-like the carrier of (X) -defined the carrier of (X) -valued Element of bool [: the carrier of (X), the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is Relation-like set
bool [: the carrier of (X), the carrier of (X):] is non empty 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 Relation-like set
bool [: the carrier of (Y), the carrier of (Y):] is non empty set
L is set
C is set
[L,C] is set
{L,C} is non empty set
{L} is non empty set
{{L,C},{L}} is non empty set
D is Element of the carrier of (X)
D is Element of the carrier of (X)
{D} is non empty set
M is Element of bool the carrier of X
Cl M is closed Element of bool the carrier of X
N is Element of the carrier of (Y)
M is Element of bool the carrier of Y
Cl M is closed Element of bool the carrier of Y
V is Element of the carrier of (Y)
D is Element of the carrier of (Y)
D is Element of the carrier of (Y)
{D} is non empty set
M is Element of bool the carrier of Y
Cl M is closed Element of bool the carrier of Y
N is Element of the carrier of (X)
M is Element of bool the carrier of X
Cl M is closed Element of bool the carrier of X
V is Element of the carrier of (X)
X is non empty set
Y is non empty TopSpace-like TopStruct

{Y} is non empty set
[:X,{Y}:] is Relation-like non empty set
bool [:X,{Y}:] is non empty set
product (X --> Y) is non empty strict TopSpace-like V213() TopStruct
((product (X --> Y))) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of ((product (X --> Y))) is non empty set
the InternalRel of ((product (X --> Y))) is Relation-like the carrier of ((product (X --> Y))) -defined the carrier of ((product (X --> Y))) -valued Element of bool [: the carrier of ((product (X --> Y))), the carrier of ((product (X --> Y))):]
[: the carrier of ((product (X --> Y))), the carrier of ((product (X --> Y))):] is Relation-like non empty set
bool [: the carrier of ((product (X --> Y))), the carrier of ((product (X --> Y))):] is non empty set
RelStr(# the carrier of ((product (X --> Y))), the InternalRel of ((product (X --> Y))) #) is non empty strict reflexive transitive RelStr

{(Y)} is non empty set
[:X,{(Y)}:] is Relation-like non empty set
bool [:X,{(Y)}:] is non empty set
product (X --> (Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of (product (X --> (Y))) is non empty set
the InternalRel of (product (X --> (Y))) is Relation-like the carrier of (product (X --> (Y))) -defined the carrier of (product (X --> (Y))) -valued Element of bool [: the carrier of (product (X --> (Y))), the carrier of (product (X --> (Y))):]
[: the carrier of (product (X --> (Y))), the carrier of (product (X --> (Y))):] is Relation-like non empty set
bool [: the carrier of (product (X --> (Y))), the carrier of (product (X --> (Y))):] is non empty set
RelStr(# the carrier of (product (X --> (Y))), the InternalRel of (product (X --> (Y))) #) is non empty strict reflexive transitive RelStr

dom (Carrier (X --> Y)) is Element of bool X
bool X is non empty set
Carrier (X --> (Y)) is Relation-like X -defined Function-like V24(X) set
dom (Carrier (X --> (Y))) is Element of bool X
L is set
(Carrier (X --> Y)) . L is set
(Carrier (X --> (Y))) . L is set
(X --> Y) . L is set
C is 1-sorted
the carrier of C is set
(X --> (Y)) . L is set
D is 1-sorted
the carrier of D is set
the carrier of Y is non empty set
the carrier of (Y) is non empty set
the carrier of (product (X --> Y)) is non empty set
product (Carrier (X --> Y)) is set
product (Carrier (X --> (Y))) is set
L is set
C is set
[L,C] is set
{L,C} is non empty set
{L} is non empty set
{{L,C},{L}} is non empty set
D is Element of the carrier of (product (X --> (Y)))

dom M is set
D is Element of the carrier of (product (X --> (Y)))

dom P is set
M is Element of the carrier of ((product (X --> Y)))
M is Element of the carrier of ((product (X --> Y)))
bool the carrier of (product (X --> Y)) is non empty set
V is Element of the carrier of (product (X --> Y))
{V} is non empty compact Element of bool the carrier of (product (X --> Y))
N is Element of the carrier of (product (X --> Y))
A is set
(X --> (Y)) . A is set
M . A is set
P . A is set
i is Element of X
N . i is Element of the carrier of Y
the carrier of Y is non empty set
V . i is Element of the carrier of Y
the carrier of (Y) is non empty set
g99 is Element of the carrier of (Y)
t9 is Element of the carrier of (Y)
{(V . i)} is non empty compact Element of bool the carrier of Y
bool the carrier of Y is non empty set
Cl {(V . i)} is closed Element of bool the carrier of Y
i is Element of bool the carrier of (product (X --> Y))
Cl i is closed Element of bool the carrier of (product (X --> Y))
D is Element of the carrier of (product (X --> (Y)))
D is Element of the carrier of (product (X --> (Y)))