:: 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
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V33() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V33() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V33() set
1 is non empty set
{{},1} is non empty set
bool K176() is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V72() normal T_3 T_4 locally-compact compact TopStruct
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
{{}} is functional non empty set
K462({{}}) is M29({{}})
[:K462({{}}),{{}}:] is Relation-like set
bool [:K462({{}}),{{}}:] is non empty set
K39(K462({{}}),{{}}) is set
Sierpinski_Space is non empty strict TopSpace-like T_0 injective TopStruct
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V33() Element of K176()
{0,1} is non empty set
{1} is non empty set
{{},{1},{0,1}} is non empty set
BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete V347() V354() V355() V356() V357() V358() satisfying_axiom_of_approximation continuous V409() V410() RelStr
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
[#] Sierpinski_Space is non empty non proper open closed dense non boundary Element of bool the carrier of Sierpinski_Space
([#] Sierpinski_Space) \ {Y} is Element of bool the carrier of Sierpinski_Space
L is set
L is set
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool (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
[#] Sierpinski_Space is non empty non proper open closed dense non boundary Element of bool the carrier of Sierpinski_Space
([#] Sierpinski_Space) \ {Y} is Element of bool the carrier of Sierpinski_Space
{0} is functional non empty set
L is set
L is set
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool (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
Cl {Y} is closed Element of bool the carrier of Sierpinski_Space
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
Cl {Y} is closed Element of bool the carrier of Sierpinski_Space
X is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict Scott TopRelStr is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict Scott TopRelStr
L is non empty set
L --> (BoolePoset 1) is Relation-like L -defined {(BoolePoset 1)} -valued Function-like constant non empty V24(L) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding Element of bool [:L,{(BoolePoset 1)}:]
{(BoolePoset 1)} is non empty set
[:L,{(BoolePoset 1)}:] is Relation-like non empty set
bool [:L,{(BoolePoset 1)}:] is non empty set
product (L --> (BoolePoset 1)) is non empty V213() strict reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
L --> Sierpinski_Space is Relation-like L -defined {Sierpinski_Space} -valued Function-like constant non empty V24(L) quasi_total V395() non-Empty TopStruct-yielding Element of bool [:L,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty set
[:L,{Sierpinski_Space}:] is Relation-like non empty set
bool [:L,{Sierpinski_Space}:] is non empty set
product (L --> Sierpinski_Space) is non empty strict TopSpace-like T_0 V213() TopStruct
the carrier of (product (L --> Sierpinski_Space)) is non empty set
C is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous TopAugmentation of product (L --> (BoolePoset 1))
the carrier of C is non empty set
Carrier (L --> (BoolePoset 1)) is Relation-like L -defined Function-like V24(L) set
dom (Carrier (L --> (BoolePoset 1))) is Element of bool L
bool L is non empty set
Carrier (L --> Sierpinski_Space) is Relation-like L -defined Function-like V24(L) set
dom (Carrier (L --> Sierpinski_Space)) is Element of bool L
D is set
(Carrier (L --> (BoolePoset 1))) . D is set
(Carrier (L --> Sierpinski_Space)) . D is set
(L --> Sierpinski_Space) . D is set
(L --> (BoolePoset 1)) . D is set
the carrier of (BoolePoset 1) 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 --> (BoolePoset 1))) is non empty set
the InternalRel of (product (L --> (BoolePoset 1))) is Relation-like the carrier of (product (L --> (BoolePoset 1))) -defined the carrier of (product (L --> (BoolePoset 1))) -valued Element of bool [: the carrier of (product (L --> (BoolePoset 1))), the carrier of (product (L --> (BoolePoset 1))):]
[: the carrier of (product (L --> (BoolePoset 1))), the carrier of (product (L --> (BoolePoset 1))):] is Relation-like non empty set
bool [: the carrier of (product (L --> (BoolePoset 1))), the carrier of (product (L --> (BoolePoset 1))):] is non empty set
RelStr(# the carrier of (product (L --> (BoolePoset 1))), the InternalRel of (product (L --> (BoolePoset 1))) #) 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 --> (BoolePoset 1))) is set
product (Carrier (L --> Sierpinski_Space)) is set
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
Y is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
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 non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
the carrier of L is non empty set
C is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of Y
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:]
D " is Relation-like Function-like set
rng D is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
[#] C is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins Element of bool the carrier of C
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
[#] L is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins Element of bool the carrier of L
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
Y is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
L is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
C is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of Y
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 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
Y is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
L is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
C is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of Y
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 (Image L) is non empty set
[: the carrier of (Image L), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (Image L), the carrier of X:] is non empty set
C is Relation-like the carrier of (Image L) -defined the carrier of X -valued Function-like non empty V24( the carrier of (Image L)) quasi_total Element of bool [: the carrier of (Image L), the carrier of X:]
corestr L is Relation-like the carrier of Y -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of Y) quasi_total onto Element of bool [: the carrier of Y, the carrier of (Image L):]
[: the carrier of Y, the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of Y, the carrier of (Image L):] is non empty set
C " is Relation-like the carrier of X -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image L):]
[: the carrier of X, the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of X, the carrier of (Image L):] is non empty set
incl (Image L) is Relation-like the carrier of (Image L) -defined the carrier of Y -valued Function-like non empty V24( the carrier of (Image L)) quasi_total continuous Element of bool [: the carrier of (Image L), the carrier of Y:]
[: the carrier of (Image L), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (Image L), the carrier of Y:] is non empty set
(incl (Image L)) * (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 * (corestr 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:]
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
(corestr L) * ((incl (Image L)) * (C ")) is Relation-like the carrier of X -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image L):]
C * ((corestr L) * ((incl (Image L)) * (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:]
(corestr L) * (incl (Image L)) is Relation-like the carrier of (Image L) -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of (Image L)) quasi_total Element of bool [: the carrier of (Image L), the carrier of (Image L):]
[: the carrier of (Image L), the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of (Image L), the carrier of (Image L):] is non empty set
((corestr L) * (incl (Image L))) * (C ") is Relation-like the carrier of X -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image L):]
C * (((corestr L) * (incl (Image L))) * (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 (Image L) is Relation-like the carrier of (Image L) -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of (Image L)) quasi_total continuous open Element of bool [: the carrier of (Image L), the carrier of (Image L):]
id the carrier of (Image L) is Relation-like the carrier of (Image L) -defined the carrier of (Image L) -valued Function-like one-to-one non empty V24( the carrier of (Image L)) quasi_total Element of bool [: the carrier of (Image L), the carrier of (Image L):]
(id (Image L)) * (C ") is Relation-like the carrier of X -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image L):]
C * ((id (Image L)) * (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 (Image D) is non empty set
[: the carrier of X, the carrier of (Image D):] is Relation-like non empty set
bool [: the carrier of X, the carrier of (Image D):] is non empty set
corestr L is Relation-like the carrier of X -defined the carrier of (Image L) -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):]
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 (Image L) is non empty set
[: the carrier of X, the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of X, the carrier of (Image L):] is non empty set
id (Image L) is Relation-like the carrier of (Image L) -defined the carrier of (Image L) -valued Function-like non empty V24( the carrier of (Image L)) quasi_total continuous open Element of bool [: the carrier of (Image L), the carrier of (Image L):]
[: the carrier of (Image L), the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of (Image L), the carrier of (Image L):] is non empty set
id the carrier of (Image L) is Relation-like the carrier of (Image L) -defined the carrier of (Image L) -valued Function-like one-to-one non empty V24( the carrier of (Image L)) quasi_total Element of bool [: the carrier of (Image L), the carrier of (Image L):]
[: the carrier of (Image L), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (Image L), the carrier of Y:] is non empty set
[: the carrier of (Image D), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (Image D), the carrier of X:] is non empty set
C * (id (Image L)) is Relation-like the carrier of (Image L) -defined the carrier of X -valued Function-like Element of bool [: the carrier of (Image L), the carrier of X:]
[: the carrier of (Image L), the carrier of X:] is Relation-like non empty set
bool [: the carrier of (Image L), 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 (Image D) -defined the carrier of X -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of X:]
V is Element of bool the carrier of X
N " V is Element of bool the carrier of (Image D)
bool the carrier of (Image D) is non empty set
dom (id (Image L)) is non empty Element of bool the carrier of (Image L)
bool the carrier of (Image L) is non empty set
[#] (Image L) is non empty non proper open closed dense non boundary Element of bool the carrier of (Image L)
C " V is Element of bool the carrier of Y
(id (Image L)) " (C " V) is Element of bool the carrier of (Image L)
(C " V) /\ ([#] (Image L)) is Element of bool the carrier of (Image L)
M is set
(id (Image L)) . M is set
M is set
(id (Image L)) . 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 (Image D) is non empty Element of bool (bool the carrier of (Image D))
bool (bool the carrier of (Image D)) is non empty set
D is Relation-like the carrier of X -defined the carrier of (Image D) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image D):]
D " is Relation-like the carrier of (Image D) -defined the carrier of X -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of X:]
D * (D ") is Relation-like the carrier of (Image D) -defined the carrier of (Image D) -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of (Image D):]
[: the carrier of (Image D), the carrier of (Image D):] is Relation-like non empty set
bool [: the carrier of (Image D), the carrier of (Image D):] is non empty set
C * (D * (D ")) is Relation-like the carrier of (Image D) -defined the carrier of X -valued Function-like Element of bool [: the carrier of (Image D), the carrier of X:]
(id X) * (D ") is Relation-like the carrier of (Image D) -defined the carrier of X -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), 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 (Image D) -defined the carrier of X -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of X:]
dom V is non empty Element of bool the carrier of (Image D)
bool the carrier of (Image D) is non empty set
[#] (Image D) is non empty non proper open closed dense non boundary Element of bool the carrier of (Image D)
rng V is non empty Element of bool the carrier of X
V " is Relation-like the carrier of X -defined the carrier of (Image D) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Image D):]
rng (corestr L) is non empty Element of bool the carrier of (Image L)
bool the carrier of (Image L) is non empty set
[#] (Image L) is non empty non proper open closed dense non boundary Element of bool the carrier of (Image L)
(corestr L) " is Relation-like Function-like set
C * (id the carrier of (Image L)) is Relation-like the carrier of (Image L) -defined the carrier of X -valued Function-like Element of bool [: the carrier of (Image L), 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 (Image D) is non empty set
[: the carrier of (Image D), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (Image D), the carrier of Y:] is non empty set
D is Relation-like the carrier of (Image D) -defined the carrier of Y -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of Y:]
C * D is Relation-like the carrier of (Image D) -defined the carrier of L -valued Function-like non empty V24( the carrier of (Image D)) quasi_total Element of bool [: the carrier of (Image D), the carrier of L:]
[: the carrier of (Image D), the carrier of L:] is Relation-like non empty set
bool [: the carrier of (Image D), 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 (Image L) -valued Function-like non empty V24( the carrier of Y) quasi_total onto Element of bool [: the carrier of Y, the carrier of (Image L):]
the carrier of (Image L) is non empty set
[: the carrier of Y, the carrier of (Image L):] is Relation-like non empty set
bool [: the carrier of Y, the carrier of (Image L):] is non empty set
D is Element of the carrier of Y
(corestr L) . D is Element of the carrier of (Image L)
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
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
Y is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous TopAugmentation of X
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 .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : a₁ in b₁ } is set
"\/" ( { (inf (C .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : a₁ in b₁ } ,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
M is open upper inaccessible_by_directed_joins Element of bool the carrier of Y
N " M is Element of bool the carrier of D
M is set
M is Element of the carrier of D
{ (inf (C .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : M in b₁ } 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 .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : t9 in b₁ } is set
"\/" ( { (inf (C .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : t9 in b₁ } ,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 .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : M in b₁ } 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 " (wayabove g) is Element of bool the carrier of L
C .: (C " (wayabove g)) is Element of bool the carrier of Y
inf (wayabove g) is Element of the carrier of Y
inf (C .: (C " (wayabove g))) is Element of the carrier of Y
[#] Y is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins Element of bool 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 .: (b₁ /\ the carrier of L))) where b₁ is open Element of bool the carrier of D : M in b₁ } ,Y) is Element of the carrier of Y
[#] Y is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins Element of bool 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 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
Y is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete satisfying_axiom_of_approximation continuous TopAugmentation of X
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
L 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
Y is strict TopRelStr
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
L 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
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 empty trivial V56() {} -element T_0 TopStruct
(X) is strict TopRelStr
the carrier of (X) is set
the carrier of X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V33() V41() 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 TopSpace-like TopStruct
(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
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
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
X is 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
Y is 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
(X) is TopSpace-like reflexive transitive strict TopRelStr
(Y) is TopSpace-like reflexive transitive strict TopRelStr
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
X --> Y is Relation-like X -defined {Y} -valued Function-like constant non empty V24(X) quasi_total V395() non-Empty TopStruct-yielding Element of bool [:X,{Y}:]
{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 TopSpace-like reflexive transitive strict TopRelStr
X --> (Y) is Relation-like X -defined {(Y)} -valued Function-like constant non empty V24(X) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding TopStruct-yielding Element of bool [:X,{(Y)}:]
{(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
Carrier (X --> Y) is Relation-like X -defined Function-like V24(X) set
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)))
M is Relation-like Function-like set
dom M is set
D is Element of the carrier of (product (X --> (Y)))
P is Relation-like Function-like set
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)))
N is Relation-like Function-like set
V is Relation-like Function-like set
M is Element of the carrier of (product (X --> Y))
the carrier of Y is non empty set
P is Element of the carrier of (product (X --> Y))
A is Element of X
M . A is Element of the carrier of Y
P . A is Element of the carrier of Y
{(P . A)} is non empty compact Element of bool the carrier of Y
bool the carrier of Y is non empty set
Cl {(P . A)} is closed Element of bool the carrier of Y
(X --> (Y)) . A is non empty reflexive RelStr
N . A is set
V . A is set
i is RelStr
the carrier of i is set
g is Element of the carrier of i
g9 is Element of the carrier of i
the carrier of (Y) is non empty set
g99 is Element of the carrier of (Y)
t9 is Element of the carrier of (Y)
{t9} is non empty compact Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
i is Element of bool the carrier of Y
Cl i is closed Element of bool the carrier of Y
{P} is non empty compact Element of bool the carrier of (product (X --> Y))
Cl {P} is closed Element of bool the carrier of (product (X --> Y))
M is Element of the carrier of ((product (X --> Y)))
M is Element of the carrier of ((product (X --> Y)))
X is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopRelStr
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of X 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
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
TopRelStr(# the carrier of X, the InternalRel of X, the topology of X #) is strict TopRelStr
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
TopStruct(# the carrier of X, the topology of X #) is non empty 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 non empty set
bool [: the carrier of (X), the carrier of (X):] is non empty set
Y is 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
D is Element of the carrier of (X)
N is Element of the carrier of (X)
{N} is non empty compact Element of bool the carrier of (X)
C is Element of the carrier of X
D is Element of the carrier of X
downarrow D is non empty directed lower Element of bool the carrier of X
{D} is non empty compact Element of bool the carrier of X
downarrow {D} is non empty lower Element of bool the carrier of X
V is Element of bool the carrier of X
Cl V is closed Element of bool the carrier of X
V is Element of the carrier of X
D is Element of the carrier of X
{D} is non empty compact Element of bool the carrier of X
C is Element of the carrier of X
downarrow D is non empty directed lower Element of bool the carrier of X
downarrow {D} is non empty lower Element of bool the carrier of X
Cl {D} is closed Element of bool the carrier of X
D is Element of the carrier of (X)
N is Element of the carrier of (X)
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
the carrier of X 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
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
Y is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
(Y) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (Y) 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 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 RelStr
the carrier of Y 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 non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopRelStr(# the carrier of Y, the InternalRel of Y, the topology of Y #) is strict TopRelStr
X is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopRelStr
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) is non empty set
the InternalRel of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) is Relation-like the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) -defined the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) -valued Element of bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X):]
[: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X):] is Relation-like non empty set
bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X):] is non empty set
RelStr(# the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X), the InternalRel of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) #) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of X 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
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 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
sigma X is Element of bool (bool the carrier of X)
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X, the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X #) is non empty strict TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
Y is non empty TopSpace-like SubSpace of X
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of Y is non empty set
the carrier of X is non empty set
the carrier of (Y) 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 non empty set
bool [: the carrier of (Y), the carrier of (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) 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
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
N is Element of the carrier of Y
{N} is non empty compact Element of bool the carrier of Y
bool the carrier of Y is non empty set
Cl {N} is closed Element of bool the carrier of Y
M is Element of the carrier of X
{M} is non empty compact Element of bool the carrier of X
bool the carrier of X is non empty set
Cl {M} is closed Element of bool the carrier of X
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
(Cl {M}) /\ ([#] Y) is Element of bool the carrier of Y
D is Element of the carrier of (Y)
D is Element of the carrier of (Y)
{D} is non empty compact Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
V is Element of the carrier of (X)
M is Element of the carrier of (X)
M is Element of bool the carrier of Y
Cl M is closed Element of bool the carrier of Y
the InternalRel of (X) |_2 the carrier 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 InternalRel of (X) /\ [: the carrier of (Y), the carrier of (Y):] is Relation-like the carrier of (X) -defined the carrier of (X) -valued 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
N is Element of the carrier of (X)
V is Element of the carrier of (X)
bool the carrier of X is non empty set
D is Element of the carrier of X
{D} is non empty compact Element of bool the carrier of X
D is Element of the carrier of X
M is Element of the carrier of Y
{M} is non empty compact Element of bool the carrier of Y
bool the carrier of Y is non empty set
Cl {M} is closed Element of bool the carrier of Y
Cl {D} is closed Element of bool the carrier of X
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
(Cl {D}) /\ ([#] Y) is Element of bool the carrier of Y
M is Element of the carrier of Y
A is Element of bool the carrier of X
Cl A is closed Element of bool the carrier of X
M is Element of the carrier of (Y)
P is Element of the carrier of (Y)
X is TopSpace-like TopStruct
the carrier of X is set
Y is TopSpace-like TopStruct
the carrier of Y is set
[: the carrier of X, the carrier of Y:] is Relation-like set
bool [: the carrier of X, the carrier of Y:] is non empty set
(X) is TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is set
(Y) is TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Y) is set
[: the carrier of (X), the carrier of (Y):] is Relation-like 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 quasi_total Element of bool [: the carrier of X, the carrier of Y:]
C is Relation-like the carrier of (X) -defined the carrier of (Y) -valued Function-like quasi_total Element of bool [: the carrier of (X), the carrier of (Y):]
dom L is Element of bool the carrier of X
bool the carrier of X is non empty set
[#] X is non proper open closed dense Element of bool the carrier of X
rng L is Element of bool the carrier of Y
bool the carrier of Y is non empty set
[#] Y is non proper open closed dense Element of bool the carrier of Y
D is non empty TopSpace-like TopStruct
(D) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (D) is non empty set
D is non empty TopSpace-like TopStruct
(D) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (D) is non empty set
[: the carrier of (D), the carrier of (D):] is Relation-like non empty set
bool [: the carrier of (D), the carrier of (D):] is non empty set
N is Relation-like the carrier of (D) -defined the carrier of (D) -valued Function-like non empty V24( the carrier of (D)) quasi_total Element of bool [: the carrier of (D), the carrier of (D):]
V is Element of the carrier of (D)
M is Element of the carrier of (D)
N . V is Element of the carrier of (D)
N . M is Element of the carrier of (D)
dom N is non empty Element of bool the carrier of (D)
bool the carrier of (D) is non empty set
the carrier of D is non empty set
bool the carrier of D is non empty set
N " is Relation-like the carrier of (D) -defined the carrier of (D) -valued Function-like non empty V24( the carrier of (D)) quasi_total Element of bool [: the carrier of (D), the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is Relation-like non empty set
bool [: the carrier of (D), the carrier of (D):] is non empty set
(N ") . (N . M) is Element of the carrier of (D)
{((N ") . (N . M))} is non empty compact Element of bool the carrier of (D)
L " is Relation-like the carrier of Y -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is Relation-like set
bool [: the carrier of Y, the carrier of X:] is non empty set
N " is Relation-like Function-like set
L " is Relation-like Function-like set
L . M is set
(L ") . (L . M) is set
the carrier of D is non empty set
bool the carrier of D is non empty set
{(N . M)} is non empty compact Element of bool the carrier of (D)
bool the carrier of (D) is non empty set
{M} is non empty compact Element of bool the carrier of (D)
P is Element of bool the carrier of D
Cl P is closed Element of bool the carrier of D
Im (L,M) is set
{M} is non empty set
L .: {M} is set
M is Element of bool the carrier of D
N .: (Cl P) is Element of bool the carrier of (D)
L . V is set
L .: P is Element of bool the carrier of Y
Cl (L .: P) is closed Element of bool the carrier of Y
M is Element of bool the carrier of D
Cl M is closed Element of bool the carrier of D
(N ") . (N . V) is Element of the carrier of (D)
(N ") .: (Cl M) is Element of bool the carrier of (D)
(L ") . (L . V) is set
(L ") .: M is Element of bool the carrier of X
Cl ((L ") .: M) is closed Element of bool the carrier of X
(N ") .: M is Element of bool the carrier of (D)
N " M is Element of bool the carrier of (D)
M is Element of bool the carrier of D
D is empty trivial V56() {} -element TopSpace-like T_0 TopStruct
(D) is empty trivial V56() {} -element TopSpace-like T_0 reflexive transitive V312() V313() V314() strict TopRelStr
D is empty trivial V56() {} -element TopSpace-like T_0 TopStruct
(D) is empty trivial V56() {} -element TopSpace-like T_0 reflexive transitive V312() V313() V314() strict TopRelStr
X is TopSpace-like TopStruct
Y is TopSpace-like TopStruct
(X) is TopSpace-like reflexive transitive strict TopRelStr
(Y) is TopSpace-like reflexive transitive strict TopRelStr
the carrier of X is set
the carrier of Y is set
[: the carrier of X, the carrier of Y:] is Relation-like 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 quasi_total Element of bool [: the carrier of X, the carrier of Y:]
the carrier of (Y) is set
the carrier of (X) is set
[: the carrier of (X), the carrier of (Y):] is Relation-like set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
C is Relation-like the carrier of (X) -defined the carrier of (Y) -valued Function-like quasi_total Element of bool [: the carrier of (X), the carrier of (Y):]
X is non empty RelStr
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
Y is non empty RelStr
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
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:]
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr
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:]
RelStr(# the carrier of Y, the InternalRel of Y #) is non empty strict RelStr
L 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 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:]
X is non empty TopSpace-like T_0 injective TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
C is non empty set
C --> Sierpinski_Space is Relation-like C -defined {Sierpinski_Space} -valued Function-like constant non empty V24(C) quasi_total V395() non-Empty TopStruct-yielding Element of bool [:C,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty set
[:C,{Sierpinski_Space}:] is Relation-like non empty set
bool [:C,{Sierpinski_Space}:] is non empty set
product (C --> Sierpinski_Space) is non empty strict TopSpace-like T_0 V213() TopStruct
the carrier of (product (C --> Sierpinski_Space)) is non empty set
[: the carrier of (product (C --> Sierpinski_Space)), the carrier of (product (C --> Sierpinski_Space)):] is Relation-like non empty set
bool [: the carrier of (product (C --> Sierpinski_Space)), the carrier of (product (C --> Sierpinski_Space)):] is non empty set
D is Relation-like the carrier of (product (C --> Sierpinski_Space)) -defined the carrier of (product (C --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (product (C --> Sierpinski_Space))) quasi_total Element of bool [: the carrier of (product (C --> Sierpinski_Space)), the carrier of (product (C --> Sierpinski_Space)):]
D * D is Relation-like the carrier of (product (C --> Sierpinski_Space)) -defined the carrier of (product (C --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (product (C --> Sierpinski_Space))) quasi_total Element of bool [: the carrier of (product (C --> Sierpinski_Space)), the carrier of (product (C --> Sierpinski_Space)):]
Image D is non empty TopSpace-like T_0 SubSpace of product (C --> Sierpinski_Space)
rng D is non empty Element of bool the carrier of (product (C --> Sierpinski_Space))
bool the carrier of (product (C --> Sierpinski_Space)) is non empty set
(product (C --> Sierpinski_Space)) | (rng D) is non empty strict TopSpace-like T_0 SubSpace of product (C --> Sierpinski_Space)
((Image D)) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of ((Image D)) is non empty set
the InternalRel of ((Image D)) is Relation-like the carrier of ((Image D)) -defined the carrier of ((Image D)) -valued Element of bool [: the carrier of ((Image D)), the carrier of ((Image D)):]
[: the carrier of ((Image D)), the carrier of ((Image D)):] is Relation-like non empty set
bool [: the carrier of ((Image D)), the carrier of ((Image D)):] is non empty set
RelStr(# the carrier of ((Image D)), the InternalRel of ((Image D)) #) is non empty strict reflexive transitive antisymmetric RelStr
((product (C --> Sierpinski_Space))) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the InternalRel of ((product (C --> Sierpinski_Space))) is Relation-like the carrier of ((product (C --> Sierpinski_Space))) -defined the carrier of ((product (C --> Sierpinski_Space))) -valued Element of bool [: the carrier of ((product (C --> Sierpinski_Space))), the carrier of ((product (C --> Sierpinski_Space))):]
the carrier of ((product (C --> Sierpinski_Space))) is non empty set
[: the carrier of ((product (C --> Sierpinski_Space))), the carrier of ((product (C --> Sierpinski_Space))):] is Relation-like non empty set
bool [: the carrier of ((product (C --> Sierpinski_Space))), the carrier of ((product (C --> Sierpinski_Space))):] is non empty set
the InternalRel of ((product (C --> Sierpinski_Space))) |_2 the carrier of ((Image D)) is Relation-like the carrier of ((Image D)) -defined the carrier of ((Image D)) -valued Element of bool [: the carrier of ((Image D)), the carrier of ((Image D)):]
the InternalRel of ((product (C --> Sierpinski_Space))) /\ [: the carrier of ((Image D)), the carrier of ((Image D)):] is Relation-like the carrier of ((product (C --> Sierpinski_Space))) -defined the carrier of ((product (C --> Sierpinski_Space))) -valued set
C --> (BoolePoset 1) is Relation-like C -defined {(BoolePoset 1)} -valued Function-like constant non empty V24(C) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding Element of bool [:C,{(BoolePoset 1)}:]
{(BoolePoset 1)} is non empty set
[:C,{(BoolePoset 1)}:] is Relation-like non empty set
bool [:C,{(BoolePoset 1)}:] is non empty set
product (C --> (BoolePoset 1)) is non empty V213() strict reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1))
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)):]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)):] is Relation-like non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)):] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the carrier of (product (C --> (BoolePoset 1))) is non empty set
the InternalRel of (product (C --> (BoolePoset 1))) is Relation-like the carrier of (product (C --> (BoolePoset 1))) -defined the carrier of (product (C --> (BoolePoset 1))) -valued Element of bool [: the carrier of (product (C --> (BoolePoset 1))), the carrier of (product (C --> (BoolePoset 1))):]
[: the carrier of (product (C --> (BoolePoset 1))), the carrier of (product (C --> (BoolePoset 1))):] is Relation-like non empty set
bool [: the carrier of (product (C --> (BoolePoset 1))), the carrier of (product (C --> (BoolePoset 1))):] is non empty set
RelStr(# the carrier of (product (C --> (BoolePoset 1))), the InternalRel of (product (C --> (BoolePoset 1))) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)))
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1))) is non empty set
the topology of (product (C --> Sierpinski_Space)) is non empty Element of bool (bool the carrier of (product (C --> Sierpinski_Space)))
bool (bool the carrier of (product (C --> Sierpinski_Space))) is non empty set
N is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) -valued Function-like non empty V24( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1))) quasi_total Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)):]
V is Relation-like the carrier of (product (C --> (BoolePoset 1))) -defined the carrier of (product (C --> (BoolePoset 1))) -valued Function-like non empty V24( the carrier of (product (C --> (BoolePoset 1)))) quasi_total idempotent monotone projection Element of bool [: the carrier of (product (C --> (BoolePoset 1))), the carrier of (product (C --> (BoolePoset 1))):]
Image V is strict reflexive transitive antisymmetric full SubRelStr of product (C --> (BoolePoset 1))
rng V is non empty Element of bool the carrier of (product (C --> (BoolePoset 1)))
bool the carrier of (product (C --> (BoolePoset 1))) is non empty set
subrelstr (rng V) is strict reflexive transitive antisymmetric full SubRelStr of product (C --> (BoolePoset 1))
the carrier of (Image V) is set
the InternalRel of (Image V) is Relation-like the carrier of (Image V) -defined the carrier of (Image V) -valued Element of bool [: the carrier of (Image V), the carrier of (Image V):]
[: the carrier of (Image V), the carrier of (Image V):] is Relation-like set
bool [: the carrier of (Image V), the carrier of (Image V):] is non empty set
the InternalRel of (product (C --> (BoolePoset 1))) |_2 the carrier of (Image V) is Relation-like the carrier of (Image V) -defined the carrier of (Image V) -valued Element of bool [: the carrier of (Image V), the carrier of (Image V):]
the InternalRel of (product (C --> (BoolePoset 1))) /\ [: the carrier of (Image V), the carrier of (Image V):] is Relation-like the carrier of (product (C --> (BoolePoset 1))) -defined the carrier of (product (C --> (BoolePoset 1))) -valued set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) is non empty strict TopSpace-like injective TopStruct
the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) is non empty set
the topology of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) is non empty Element of bool (bool the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #))
bool the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #)) is non empty set
TopStruct(# the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #), the topology of TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #) #) is non empty strict TopSpace-like injective TopStruct
(TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1)) #)) is non empty TopSpace-like reflexive transitive strict TopRelStr
( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective TopAugmentation of product (C --> (BoolePoset 1))) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict TopRelStr
TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #) is non empty strict TopSpace-like TopStruct
(TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) is non empty set
the InternalRel of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) is Relation-like the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) -defined the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) -valued Element of bool [: the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)), the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)):]
[: the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)), the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)):] is Relation-like non empty set
bool [: the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)), the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)):] is non empty set
RelStr(# the carrier of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)), the InternalRel of (TopStruct(# the carrier of (product (C --> Sierpinski_Space)), the topology of (product (C --> Sierpinski_Space)) #)) #) is non empty strict reflexive transitive RelStr
the carrier of (Image D) is non empty set
X is non empty TopSpace-like T_0 injective TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
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 continuous Element of bool [: the carrier of (X), the carrier of (Y):]
C is Element of the carrier of (X)
D is Element of the carrier of (X)
L . C is Element of the carrier of (Y)
L . D is Element of the carrier of (Y)
the carrier of Y is non empty set
bool the carrier of Y is non empty set
L . D is Element of the carrier of (Y)
{(L . D)} is non empty compact Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
{D} is non empty compact Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
N is Element of bool the carrier of X
Cl N is closed Element of bool the carrier of X
L . C is Element of the carrier of (Y)
D is Element of bool the carrier of Y
[: 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
M is Element of bool the carrier of Y
V 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:]
V " M is Element of bool the carrier of X
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the topology of (Y) is non empty Element of bool (bool the carrier of (Y))
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y), the topology of (Y) #) is non empty strict TopSpace-like TopStruct
the 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
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
N /\ (V " M) is Element of bool the carrier of X
M is set
D /\ M is Element of bool the carrier of Y
{} Y is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper Function-yielding V33() open closed boundary nowhere_dense Element of bool the carrier of Y
Cl D is closed Element of bool the carrier of Y
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
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):]
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
{Y} is non empty compact Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
Cl {Y} is closed Element of bool the carrier of (X)
downarrow Y is non empty directed lower Element of bool the carrier of (X)
downarrow {Y} is non empty lower Element of bool the carrier of (X)
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
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
C is set
L is Element of bool the carrier of X
Cl L is closed Element of bool the carrier of X
D is Element of the carrier of (X)
L is set
C is Element of the carrier of (X)
D is Element of bool the carrier of X
Cl D is closed Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
{Y} is non empty compact Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
Cl {Y} is closed Element of bool the carrier of (X)
L is Element of the carrier of (X)
{L} is non empty compact Element of bool the carrier of (X)
Cl {L} is closed Element of bool the carrier of (X)
downarrow L is non empty directed lower Element of bool the carrier of (X)
downarrow {L} is non empty lower Element of bool the carrier of (X)
downarrow Y is non empty directed lower Element of bool the carrier of (X)
downarrow {Y} is non empty lower Element of bool the carrier of (X)
X is TopSpace-like TopStruct
(X) is TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is set
bool the carrier of (X) is non empty set
Y is open Element of bool the carrier of (X)
L is Element of the carrier of (X)
C is Element of the carrier of (X)
the carrier of X is set
bool the carrier of X is non empty set
{C} is non empty set
D is Element of bool the carrier of X
Cl D is closed Element of bool the carrier of X
D is non empty TopSpace-like TopStruct
(D) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (D) is non empty set
the carrier of D is non empty set
the topology of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D, the topology of D #) is non empty strict TopSpace-like TopStruct
the topology of (D) is non empty Element of bool (bool the carrier of (D))
bool the carrier of (D) is non empty set
bool (bool the carrier of (D)) is non empty set
TopStruct(# the carrier of (D), the topology of (D) #) is non empty strict TopSpace-like TopStruct
D is Element of the carrier of (D)
{D} is non empty compact Element of bool the carrier of (D)
Cl {D} is non empty closed closed directed lower Element of bool the carrier of (D)
N is Element of bool the carrier of X
Cl N is closed Element of bool the carrier of X
X is TopSpace-like TopStruct
(X) is TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of (X)
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of Y is non empty set
the carrier of (Y) is non empty set
the carrier of (ContMaps (X,(Y))) is non empty set
the carrier of X is non empty set
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
C is 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):]
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the carrier of L is non empty set
Funcs ( the carrier of L, the carrier of (ContMaps (X,(Y)))) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of (ContMaps (X,(Y)))
Funcs ( the carrier of L,(Funcs ( the carrier of X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of L, Funcs ( the carrier of X, the carrier of Y)
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
L is non empty RelStr
X is non empty set
the carrier of L is non empty set
Y is non empty RelStr
Y |^ X is non empty V213() strict RelStr
the carrier of (Y |^ X) is non empty set
C is non empty transitive directed NetStr over L
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 transitive RelStr
the mapping of C 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:]
[: 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
commute the mapping of C is Relation-like Function-like Function-yielding V33() set
D is Element of X
(commute the mapping of C) . D is Relation-like Function-like set
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of X, the carrier of Y
Funcs ( the carrier of C, the carrier of L) is functional non empty FUNCTION_DOMAIN of the carrier of C, the carrier of L
Funcs ( the carrier of C,(Funcs (X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of C, Funcs (X, the carrier of Y)
rng ((commute the mapping of C) . D) is set
dom ((commute the mapping of C) . D) is 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:]
NetStr(# the carrier of C, the InternalRel of C,D #) is non empty strict NetStr over Y
the carrier of NetStr(# the carrier of C, the InternalRel of C,D #) is non empty set
the InternalRel of NetStr(# the carrier of C, the InternalRel of C,D #) is Relation-like the carrier of NetStr(# the carrier of C, the InternalRel of C,D #) -defined the carrier of NetStr(# the carrier of C, the InternalRel of C,D #) -valued Element of bool [: the carrier of NetStr(# the carrier of C, the InternalRel of C,D #), the carrier of NetStr(# the carrier of C, the InternalRel of C,D #):]
[: the carrier of NetStr(# the carrier of C, the InternalRel of C,D #), the carrier of NetStr(# the carrier of C, the InternalRel of C,D #):] is Relation-like non empty set
bool [: the carrier of NetStr(# the carrier of C, the InternalRel of C,D #), the carrier of NetStr(# the carrier of C, the InternalRel of C,D #):] is non empty set
RelStr(# the carrier of NetStr(# the carrier of C, the InternalRel of C,D #), the InternalRel of NetStr(# the carrier of C, the InternalRel of C,D #) #) is non empty strict RelStr
[#] C is non empty non proper lower upper Element of bool the carrier of C
bool the carrier of C is non empty set
[#] NetStr(# the carrier of C, the InternalRel of C,D #) is non empty non proper lower upper Element of bool the carrier of NetStr(# the carrier of C, the InternalRel of C,D #)
bool the carrier of NetStr(# the carrier of C, the InternalRel of C,D #) is non empty set
V is non empty transitive strict directed NetStr over Y
the carrier of V is non empty set
the InternalRel of V is Relation-like the carrier of V -defined the carrier of V -valued Element of bool [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
RelStr(# the carrier of V, the InternalRel of V #) is non empty strict transitive RelStr
the mapping of V is Relation-like the carrier of V -defined the carrier of Y -valued Function-like non empty V24( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of Y:]
[: the carrier of V, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of V, the carrier of Y:] is non empty set
D is non empty transitive strict directed NetStr over Y
the carrier of D is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D, the InternalRel of D #) is non empty strict transitive RelStr
the mapping of 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:]
the carrier of Y 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
N is non empty transitive strict directed NetStr over Y
the carrier of N is non empty set
the InternalRel of N is Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict transitive RelStr
the mapping of N is Relation-like the carrier of N -defined the carrier of Y -valued Function-like non empty V24( the carrier of N) quasi_total Element of bool [: the carrier of N, the carrier of Y:]
[: the carrier of N, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of N, the carrier of Y:] is non empty set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of X is non empty set
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the carrier of L is non empty set
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of (ContMaps (X,(Y))) is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
C is Element of the carrier of L
the mapping of L . C is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
D is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,D) is non empty transitive strict directed NetStr over (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D) is non empty set
the carrier of (Y) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D), the carrier of (Y):] is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,D) . C is set
( the mapping of L . C) . D is set
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
Funcs ( the carrier of L,(Funcs ( the carrier of X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of L, Funcs ( the carrier of X, the carrier of Y)
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive RelStr
the carrier of ((Y) |^ the carrier of X) is non empty set
commute the mapping of L is Relation-like Function-like Function-yielding V33() set
(commute the mapping of L) . D is Relation-like Function-like set
((commute the mapping of L) . D) . C is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of X is non empty set
L is non empty transitive directed eventually-directed Function-yielding NetStr over ContMaps (X,(Y))
C is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty transitive strict directed NetStr over (Y)
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive RelStr
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty set
N is Element of the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . N is Element of the carrier of (Y)
the carrier of (Y) is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):]
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . N is Element of the carrier of (Y)
the carrier of (ContMaps (X,(Y))) is non empty set
the carrier of ((Y) |^ the carrier of X) is non empty set
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 transitive RelStr
the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -defined the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -valued Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):]
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):] is non empty set
RelStr(# the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) #) is non empty strict transitive RelStr
V is Element of the carrier of L
L . V is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
the mapping of L . V is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
M is Element of the carrier of L
M is Element of the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)
M is Element of the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . M is Element of the carrier of (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . M is Element of the carrier of (Y)
P is Element of the carrier of L
L . P is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . P is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
the carrier of X --> (Y) is Relation-like the carrier of X -defined {(Y)} -valued Function-like constant non empty V24( the carrier of X) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding TopStruct-yielding Element of bool [: the carrier of X,{(Y)}:]
{(Y)} is non empty set
[: the carrier of X,{(Y)}:] is Relation-like non empty set
bool [: the carrier of X,{(Y)}:] is non empty set
product ( the carrier of X --> (Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of (product ( the carrier of X --> (Y))) is non empty set
A is Element of the carrier of ((Y) |^ the carrier of X)
i is Element of the carrier of ((Y) |^ the carrier of X)
g is Element of the carrier of (product ( the carrier of X --> (Y)))
g9 is Element of the carrier of (product ( the carrier of X --> (Y)))
( the carrier of X --> (Y)) . C is non empty reflexive RelStr
g . C is Element of the carrier of (( the carrier of X --> (Y)) . C)
the carrier of (( the carrier of X --> (Y)) . C) is non empty set
g9 . C is Element of the carrier of (( the carrier of X --> (Y)) . C)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . P is set
the mapping of L . M is Relation-like Function-like set
( the mapping of L . M) . C is set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . V is set
the mapping of L . N is Relation-like Function-like set
( the mapping of L . N) . C is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of X is non empty set
L is non empty transitive directed eventually-directed Function-yielding NetStr over ContMaps (X,(Y))
C is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty transitive strict directed NetStr over (Y)
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the carrier of L is non empty set
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of (ContMaps (X,(Y))) is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
C is Element of the carrier of L
the mapping of L . C is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
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 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
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive RelStr
the carrier of X is non empty set
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive RelStr
the carrier of (ContMaps (X,(Y))) is non empty set
the carrier of ((Y) |^ the carrier of X) is non empty set
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
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 transitive RelStr
C is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty transitive strict directed NetStr over (Y)
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty set
the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -defined the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -valued Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):]
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C):] is non empty set
RelStr(# the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) #) is non empty strict transitive RelStr
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
dom the mapping of L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):]
the carrier of (Y) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is non empty set
dom the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) 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 T_0 TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive antisymmetric RelStr
the carrier of (ContMaps (X,(Y))) is non empty set
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of L is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
rng the mapping of L is non empty Element of bool the carrier of (ContMaps (X,(Y)))
bool the carrier of (ContMaps (X,(Y))) 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 carrier of ((Y) |^ the carrier of X) is non empty set
N is Element of the carrier of ((Y) |^ the carrier of X)
dom the mapping of L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
the carrier of X --> (Y) is Relation-like the carrier of X -defined {(Y)} -valued Function-like constant non empty V24( the carrier of X) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding TopStruct-yielding Element of bool [: the carrier of X,{(Y)}:]
{(Y)} is non empty set
[: the carrier of X,{(Y)}:] is Relation-like non empty set
bool [: the carrier of X,{(Y)}:] is non empty set
product ( the carrier of X --> (Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
V is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of (product ( the carrier of X --> (Y))) is non empty set
M is set
the mapping of L . M is Relation-like Function-like set
M is Element of the carrier of (product ( the carrier of X --> (Y)))
M is Element of the carrier of (product ( the carrier of X --> (Y)))
A is Element of the carrier of X
( the carrier of X --> (Y)) . A is non empty reflexive RelStr
M . A is Element of the carrier of (( the carrier of X --> (Y)) . A)
the carrier of (( the carrier of X --> (Y)) . A) is non empty set
M . A is Element of the carrier of (( the carrier of X --> (Y)) . A)
( the carrier of X --> (Y)) . A is non empty reflexive RelStr
( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty transitive strict directed NetStr over (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A), the carrier of (Y):] is non empty set
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
P is Element of the carrier of L
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) . P is set
dom the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty set
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is Element of the carrier of (Y)
\\/ ( the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A) is non empty set
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A)),(Y)) is Element of the carrier of (Y)
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,A)),(Y)) is Element of the carrier of (Y)
V is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of (product ( the carrier of X --> (Y))) is non empty set
M is Element of the carrier of (product ( the carrier of X --> (Y)))
M is Element of the carrier of (product ( the carrier of X --> (Y)))
M is Element of the carrier of X
( the carrier of X --> (Y)) . M is non empty reflexive RelStr
M . M is Element of the carrier of (( the carrier of X --> (Y)) . M)
the carrier of (( the carrier of X --> (Y)) . M) is non empty set
M . M is Element of the carrier of (( the carrier of X --> (Y)) . M)
( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty transitive strict directed NetStr over (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):] is non empty set
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
( the carrier of X --> (Y)) . M is non empty reflexive RelStr
V . M is Element of the carrier of (Y)
P is Element of the carrier of (Y)
dom the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
A is set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) . A is set
i is Element of the carrier of L
the mapping of L . i is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
g is Element of the carrier of ((Y) |^ the carrier of X)
g9 is Element of the carrier of (product ( the carrier of X --> (Y)))
( the mapping of L . i) . M is set
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Element of the carrier of (Y)
\\/ ( the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)),(Y)) is Element of the carrier of (Y)
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)),(Y)) is Element of the carrier of (Y)
V is Element of the carrier of ((Y) |^ 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
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
(Y) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Y) is non empty set
bool the carrier of (Y) is non empty set
L is non empty directed Element of bool the carrier of (Y)
"\/" (L,(Y)) is Element of the carrier of (Y)
C is open Element of bool the carrier of Y
D is Element of bool the carrier of X
X is non empty 1-sorted
the carrier of X is non empty set
bool the carrier of X is non empty set
L is Element of the carrier of X
{L} is non empty Element of bool the carrier of X
Y is non empty Element of bool the carrier of X
the Element of Y is Element of Y
D is set
X is non empty TopSpace-like T_0 TopStruct
the carrier of X is non empty set
Y is Element of the carrier of X
{Y} is non empty compact Element of bool the carrier of X
bool the carrier of X is non empty set
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
C is non empty directed Element of bool the carrier of (X)
"\/" (C,(X)) is Element of the carrier of (X)
L is Element of the carrier of (X)
{L} is non empty compact Element of bool the carrier of (X)
D is open Element of bool the carrier of X
X is non empty TopSpace-like T_0 () TopStruct
Y is non empty TopSpace-like T_0 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:]
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (X) is non empty set
(Y) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
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
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):]
rng C is non empty Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
D is non empty directed Element of bool the carrier of (Y)
bool the carrier of Y is non empty set
"\/" (D,(Y)) is Element of 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):]
[: 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
rng L is non empty Element of bool the carrier of Y
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
(C ") .: D is non empty Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
C " D is Element of bool the carrier of (X)
C .: (C " D) is Element of bool the carrier of (Y)
D is open Element of bool the carrier of Y
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,(Y))) is set
(L ") .: D is Element of bool the carrier of X
bool the carrier of X is non empty set
L " D is Element of bool the carrier of X
L " is Relation-like Function-like set
(L ") . ("\/" (D,(Y))) is set
(C ") . ("\/" (D,(Y))) is Element of the carrier of (X)
"\/" (((C ") .: D),(X)) is Element of the carrier of (X)
"\/" ((C " D),(X)) is Element of the carrier of (X)
N is set
V is Element of the carrier of X
L . V is Element of the carrier of Y
M is Element of the carrier of Y
M is Element of the carrier of Y
X is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopRelStr
(X) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict TopRelStr
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is non empty directed Element of bool the carrier of (X)
the carrier of X is non empty set
bool the carrier of X is non empty set
"\/" (Y,(X)) is Element of the carrier of (X)
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
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
TopRelStr(# the carrier of X, the InternalRel of X, the topology of X #) is strict TopRelStr
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
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
C is open upper inaccessible_by_directed_joins Element of bool the carrier of X
L is Element of bool the carrier of X
"\/" (L,X) is Element of the carrier of X
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
Y is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott TopAugmentation of X
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete RelStr
Y is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott () TopAugmentation of X
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
X is non empty TopSpace-like T_0 () TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is non empty directed Element of bool the carrier of (X)
X is non empty TopSpace-like T_0 () TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
Y is non empty directed eventually-directed NetStr over (X)
the carrier of (X) is non empty set
netmap (Y,(X)) 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 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
the mapping of Y 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 (netmap (Y,(X))) is non empty Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
rng the mapping of Y is non empty Element of bool the carrier of (X)
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
Y is non empty transitive directed eventually-directed NetStr over (X)
sup Y is Element of the carrier of (X)
the carrier of (X) is non empty set
Lim Y is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
netmap (Y,(X)) 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 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
the mapping of Y 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 (netmap (Y,(X))) is non empty Element of bool the carrier of (X)
rng the mapping of Y is non empty Element of bool the carrier of (X)
C is a_neighborhood of sup Y
Int C is open upper Element of bool the carrier of (X)
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
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 Element of bool the carrier of X
\\/ ( the mapping of Y,(X)) is Element of the carrier of (X)
rng the mapping of Y is non empty set
"\/" ((rng the mapping of Y),(X)) is Element of the carrier of (X)
L is non empty directed Element of bool the carrier of (X)
D is set
dom the mapping of Y is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
N is Element of the carrier of X
V is set
the mapping of Y . V is set
M is Element of the carrier of Y
Y . M is Element of the carrier of (X)
the mapping of Y . M is Element of the carrier of (X)
M is Element of the carrier of Y
M is Element of the carrier of Y
Y . M is Element of the carrier of (X)
the mapping of Y . M is Element of the carrier of (X)
{(Y . M)} is non empty compact Element of bool the carrier of (X)
P is Element of bool the carrier of X
Cl P is closed Element of bool the carrier of X
P /\ D is Element of bool the carrier of X
A is set
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
Y is non empty transitive directed eventually-directed NetStr over (X)
Lim Y is Element of bool the carrier of (X)
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
Y is non empty transitive directed eventually-directed NetStr over (X)
X is non empty TopSpace-like TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is non empty directed Element of bool the carrier of (X)
the carrier of X is non empty set
bool the carrier of X is non empty set
"\/" (Y,(X)) is Element of the carrier of (X)
Net-Str Y is non empty reflexive transitive strict directed monotone eventually-directed NetStr over (X)
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
the InternalRel of (X) |_2 Y is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
[:Y,Y:] is Relation-like non empty set
bool [:Y,Y:] is non empty set
the InternalRel of (X) /\ [:Y,Y:] is Relation-like the carrier of (X) -defined the carrier of (X) -valued 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):]
(id the carrier of (X)) | Y is Relation-like Y -defined the carrier of (X) -defined the carrier of (X) -valued Function-like non empty V24(Y) quasi_total Element of bool [:Y, the carrier of (X):]
[:Y, the carrier of (X):] is Relation-like non empty set
bool [:Y, the carrier of (X):] is non empty set
NetStr(# Y,( the InternalRel of (X) |_2 Y),((id the carrier of (X)) | Y) #) is non empty strict NetStr over (X)
the mapping of (Net-Str Y) is Relation-like the carrier of (Net-Str Y) -defined the carrier of (X) -valued Function-like non empty V24( the carrier of (Net-Str Y)) quasi_total Element of bool [: the carrier of (Net-Str Y), the carrier of (X):]
the carrier of (Net-Str Y) is non empty set
[: the carrier of (Net-Str Y), the carrier of (X):] is Relation-like non empty set
bool [: the carrier of (Net-Str Y), the carrier of (X):] is non empty set
rng the mapping of (Net-Str Y) is non empty Element of bool the carrier of (X)
L is open Element of bool the carrier of X
sup (Net-Str Y) is Element of the carrier of (X)
\\/ ( the mapping of (Net-Str Y),(X)) is Element of the carrier of (X)
rng the mapping of (Net-Str Y) is non empty set
"\/" ((rng the mapping of (Net-Str Y)),(X)) is Element of the carrier of (X)
"\/" ((rng the mapping of (Net-Str Y)),(X)) is Element of the carrier of (X)
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
C is Element of bool the carrier of (X)
Int C is open upper Element of bool the carrier of (X)
Int L is open Element of bool the carrier of X
Lim (Net-Str Y) is Element of bool the carrier of (X)
D is Element of the carrier of (Net-Str Y)
(Net-Str Y) . D is Element of the carrier of (X)
the mapping of (Net-Str Y) . D is Element of the carrier of (X)
dom the mapping of (Net-Str Y) is non empty Element of bool the carrier of (Net-Str Y)
bool the carrier of (Net-Str Y) is non empty set
D is Element of the carrier of (X)
D is Element of the carrier of (X)
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is non empty TopSpace-like T_0 TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
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 continuous monotone Element of bool [: the carrier of (X), the carrier of (Y):]
bool the carrier of (X) is non empty set
C is non empty directed Element of bool the carrier of (X)
L .: C is non empty Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
"\/" ((L .: C),(Y)) is Element of the carrier of (Y)
"\/" (C,(X)) is Element of the carrier of (X)
L . ("\/" (C,(X))) is Element of the carrier of (Y)
downarrow ("\/" ((L .: C),(Y))) is non empty closed directed directed lower lower Element of bool the carrier of (Y)
{("\/" ((L .: C),(Y)))} is non empty compact Element of bool the carrier of (Y)
downarrow {("\/" ((L .: C),(Y)))} is non empty lower Element of bool the carrier of (Y)
(downarrow ("\/" ((L .: C),(Y)))) ` is open upper Element of bool the carrier of (Y)
the carrier of (Y) \ (downarrow ("\/" ((L .: C),(Y)))) is set
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
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
L " ((downarrow ("\/" ((L .: C),(Y)))) `) is Element of bool the carrier of (X)
[#] (Y) is non empty non proper open closed dense non boundary lower upper upper Element of bool the carrier of (Y)
D is Element of bool the carrier of X
the carrier of Y is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the topology of (Y) is non empty Element of bool (bool the carrier of (Y))
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y), the topology of (Y) #) is non empty strict TopSpace-like TopStruct
L . ("\/" (C,(X))) is Element of the carrier of (Y)
V is Element of the carrier of (Y)
M is Element of the carrier of (Y)
{M} is non empty compact Element of bool the carrier of (Y)
M is Element of bool the carrier of Y
M is Element of bool the carrier of Y
P is open upper Element of bool the carrier of (Y)
L " P is Element of bool the carrier of (X)
A is set
i is Element of the carrier of (X)
L . i is Element of the carrier of (Y)
Cl M is closed Element of bool the carrier of Y
V is Element of the carrier of (Y)
L . ("\/" (C,(X))) is Element of the carrier of (Y)
N is open Element of bool the carrier of X
V is set
M is Element of the carrier of (X)
L . M is Element of the carrier of (Y)
X is non empty TopSpace-like () TopStruct
(X) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (X) is non empty set
Y is non empty TopSpace-like T_0 TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
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):]
X is non empty TopSpace-like T_0 () TopStruct
Y is non empty TopSpace-like T_0 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
[: 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
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:]
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 continuous Element of bool [: the carrier of Y, the carrier of X:]
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 continuous Element of bool [: the carrier of X, the carrier of Y:]
C * L 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 TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of (Y) is non empty set
bool the carrier of (Y) is non empty set
D is non empty directed Element of bool the carrier of (Y)
bool the carrier of Y is non empty set
"\/" (D,(Y)) is Element of the carrier of (Y)
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the topology of (Y) is non empty Element of bool (bool the carrier of (Y))
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y), the topology of (Y) #) is non empty strict TopSpace-like TopStruct
the 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 non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
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
[: 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 * C 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 X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] 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 .: D is Element of bool the carrier of X
C .: (L .: D) is Element of bool the carrier of Y
D is non empty Element of bool the carrier of Y
(C * L) .: D is non empty Element of bool the carrier of Y
[: 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
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 Element of bool [: the carrier of (Y), the carrier of (X):]
M .: D is non empty Element of bool the carrier of (X)
N 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):]
V 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):]
L . ("\/" (D,(Y))) is set
"\/" ((M .: D),(X)) is Element of the carrier of (X)
C . ("\/" ((M .: D),(X))) is set
L . (C . ("\/" ((M .: D),(X)))) is set
N . ("\/" ((M .: D),(X))) is Element of the carrier of (X)
N .: (M .: D) is non empty Element of bool the carrier of (X)
"\/" ((N .: (M .: D)),(X)) is Element of the carrier of (X)
M is open Element of bool the carrier of Y
L .: M is Element of bool the carrier of X
C " M is Element of bool the carrier of X
M is set
P is set
L . P is set
A is Element of the carrier of Y
L . A is Element of the carrier of X
C . M is set
(C * L) . A is Element of the carrier of Y
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
M is set
C . M is set
P is set
P is set
L is non empty TopSpace-like T_0 injective TopStruct
(L) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict satisfying_axiom_of_approximation continuous TopRelStr
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 injective TopStruct
C is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (L)
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 injective () TopStruct
D is non empty set
D --> Sierpinski_Space is Relation-like D -defined {Sierpinski_Space} -valued Function-like constant non empty V24(D) quasi_total V395() non-Empty TopStruct-yielding Element of bool [:D,{Sierpinski_Space}:]
{Sierpinski_Space} is non empty set
[:D,{Sierpinski_Space}:] is Relation-like non empty set
bool [:D,{Sierpinski_Space}:] is non empty set
product (D --> Sierpinski_Space) is non empty strict TopSpace-like T_0 V213() TopStruct
the carrier of (product (D --> Sierpinski_Space)) is non empty set
[: the carrier of L, the carrier of (product (D --> Sierpinski_Space)):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (product (D --> Sierpinski_Space)):] is non empty set
[: the carrier of (product (D --> Sierpinski_Space)), the carrier of L:] is Relation-like non empty set
bool [: the carrier of (product (D --> Sierpinski_Space)), the carrier of L:] is non empty set
id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total continuous open 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
id the carrier of L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of L:]
D is Relation-like the carrier of L -defined the carrier of (product (D --> Sierpinski_Space)) -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of (product (D --> Sierpinski_Space)):]
N is Relation-like the carrier of (product (D --> Sierpinski_Space)) -defined the carrier of L -valued Function-like non empty V24( the carrier of (product (D --> Sierpinski_Space))) quasi_total continuous Element of bool [: the carrier of (product (D --> Sierpinski_Space)), the carrier of L:]
N * D is Relation-like the carrier of L -defined the carrier of L -defined the carrier of L -valued the carrier of L -valued Function-like non empty V24( the carrier of L) V24( the carrier of L) quasi_total quasi_total continuous Element of bool [: the carrier of L, the carrier of L:]
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
the topology of (product (D --> Sierpinski_Space)) is non empty Element of bool (bool the carrier of (product (D --> Sierpinski_Space)))
bool the carrier of (product (D --> Sierpinski_Space)) is non empty set
bool (bool the carrier of (product (D --> Sierpinski_Space))) is non empty set
TopStruct(# the carrier of (product (D --> Sierpinski_Space)), the topology of (product (D --> Sierpinski_Space)) #) is non empty strict TopSpace-like TopStruct
((product (D --> Sierpinski_Space))) is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
the carrier of ((product (D --> Sierpinski_Space))) is non empty set
the topology of ((product (D --> Sierpinski_Space))) is non empty Element of bool (bool the carrier of ((product (D --> Sierpinski_Space))))
bool the carrier of ((product (D --> Sierpinski_Space))) is non empty set
bool (bool the carrier of ((product (D --> Sierpinski_Space)))) is non empty set
TopStruct(# the carrier of ((product (D --> Sierpinski_Space))), the topology of ((product (D --> Sierpinski_Space))) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (L), the carrier of ((product (D --> Sierpinski_Space))):] is Relation-like non empty set
bool [: the carrier of (L), the carrier of ((product (D --> Sierpinski_Space))):] is non empty set
D --> (BoolePoset 1) is Relation-like D -defined {(BoolePoset 1)} -valued Function-like constant non empty V24(D) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding Element of bool [:D,{(BoolePoset 1)}:]
{(BoolePoset 1)} is non empty set
[:D,{(BoolePoset 1)}:] is Relation-like non empty set
bool [:D,{(BoolePoset 1)}:] is non empty set
product (D --> (BoolePoset 1)) is non empty V213() strict reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):] is Relation-like non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
the carrier of (product (D --> (BoolePoset 1))) is non empty set
the InternalRel of (product (D --> (BoolePoset 1))) is Relation-like the carrier of (product (D --> (BoolePoset 1))) -defined the carrier of (product (D --> (BoolePoset 1))) -valued Element of bool [: the carrier of (product (D --> (BoolePoset 1))), the carrier of (product (D --> (BoolePoset 1))):]
[: the carrier of (product (D --> (BoolePoset 1))), the carrier of (product (D --> (BoolePoset 1))):] is Relation-like non empty set
bool [: the carrier of (product (D --> (BoolePoset 1))), the carrier of (product (D --> (BoolePoset 1))):] is non empty set
RelStr(# the carrier of (product (D --> (BoolePoset 1))), the InternalRel of (product (D --> (BoolePoset 1))) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete V357() V358() satisfying_axiom_of_approximation continuous RelStr
[: the carrier of (L), the carrier of (product (D --> (BoolePoset 1))):] is Relation-like non empty set
bool [: the carrier of (L), the carrier of (product (D --> (BoolePoset 1))):] 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 (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 the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):] is Relation-like non empty set
bool [: the carrier of C, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):] is non empty set
M is Relation-like the carrier of (L) -defined the carrier of (product (D --> (BoolePoset 1))) -valued Function-like non empty V24( the carrier of (L)) quasi_total Element of bool [: the carrier of (L), the carrier of (product (D --> (BoolePoset 1))):]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of L:] is Relation-like non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of L:] is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)))
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is non empty set
( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict satisfying_axiom_of_approximation continuous TopRelStr
the InternalRel of ((product (D --> Sierpinski_Space))) is Relation-like the carrier of ((product (D --> Sierpinski_Space))) -defined the carrier of ((product (D --> Sierpinski_Space))) -valued Element of bool [: the carrier of ((product (D --> Sierpinski_Space))), the carrier of ((product (D --> Sierpinski_Space))):]
[: the carrier of ((product (D --> Sierpinski_Space))), the carrier of ((product (D --> Sierpinski_Space))):] is Relation-like non empty set
bool [: the carrier of ((product (D --> Sierpinski_Space))), the carrier of ((product (D --> Sierpinski_Space))):] is non empty set
RelStr(# the carrier of ((product (D --> Sierpinski_Space))), the InternalRel of ((product (D --> Sierpinski_Space))) #) is non empty strict reflexive transitive antisymmetric RelStr
[: the carrier of (product (D --> (BoolePoset 1))), the carrier of (L):] is Relation-like non empty set
bool [: the carrier of (product (D --> (BoolePoset 1))), the carrier of (L):] is non empty set
the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is non empty set
the InternalRel of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is Relation-like the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) -defined the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) -valued Element of bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))):]
[: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))):] is Relation-like non empty set
bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))):] is non empty set
RelStr(# the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the InternalRel of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima V313() up-complete RelStr
[: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of (L):] is Relation-like non empty set
bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of (L):] is non empty set
i is Relation-like the carrier of (product (D --> (BoolePoset 1))) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of (product (D --> (BoolePoset 1)))) quasi_total Element of bool [: the carrier of (product (D --> (BoolePoset 1))), the carrier of (L):]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of C:] is Relation-like non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of C:] is non empty set
[: the carrier of (product (D --> Sierpinski_Space)), the carrier of C:] is Relation-like non empty set
bool [: the carrier of (product (D --> Sierpinski_Space)), the carrier of C:] is non empty set
g9 is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) -defined the carrier of C -valued Function-like non empty V24( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) quasi_total Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of C:]
the topology of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is non empty Element of bool (bool the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))))
bool the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) is non empty set
bool (bool the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)))) is non empty set
TopStruct(# the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the topology of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) #) is non empty strict TopSpace-like TopStruct
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) #) is non empty strict TopSpace-like injective () TopStruct
g is Relation-like the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)))) quasi_total Element of bool [: the carrier of ( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))), the carrier of (L):]
g99 is Relation-like the carrier of (product (D --> Sierpinski_Space)) -defined the carrier of C -valued Function-like non empty V24( the carrier of (product (D --> Sierpinski_Space))) quasi_total Element of bool [: the carrier of (product (D --> Sierpinski_Space)), the carrier of C:]
g99 * 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 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
A is non empty TopSpace-like () TopStruct
(A) is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (A) is non empty set
[: the carrier of (A), the carrier of ((product (D --> Sierpinski_Space))):] is Relation-like non empty set
bool [: the carrier of (A), the carrier of ((product (D --> Sierpinski_Space))):] is non empty set
V is Relation-like the carrier of (L) -defined the carrier of ((product (D --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (L)) quasi_total Element of bool [: the carrier of (L), the carrier of ((product (D --> Sierpinski_Space))):]
M is Relation-like the carrier of C -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) -valued Function-like non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)):]
t9 is Relation-like the carrier of (A) -defined the carrier of ((product (D --> Sierpinski_Space))) -valued Function-like non empty V24( the carrier of (A)) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of (A), the carrier of ((product (D --> Sierpinski_Space))):]
P is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)) -defined the carrier of L -valued Function-like non empty V24( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1))) quasi_total Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of product (D --> (BoolePoset 1)), the carrier of L:]
P * M 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:]
[: 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
X is non empty TopSpace-like T_0 injective TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict satisfying_axiom_of_approximation continuous TopRelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X))
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X)) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) #) is non empty strict 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 injective TopStruct
X is non empty TopSpace-like T_0 injective TopStruct
(X) is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete strict satisfying_axiom_of_approximation continuous TopRelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X))
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X)) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X), the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V312() V313() V314() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective () TopAugmentation of (X) #) is non empty strict 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 injective TopStruct
X is non empty TopSpace-like T_0 TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like T_0 () TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
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
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive antisymmetric RelStr
the carrier of (ContMaps (X,(Y))) is non empty set
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of L is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
rng the mapping of L is non empty Element of bool the carrier of (ContMaps (X,(Y)))
bool the carrier of (ContMaps (X,(Y))) is non empty set
"\/" ((rng the mapping of L),((Y) |^ the carrier of X)) is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of ((Y) |^ the carrier of X) is non empty set
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):]
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):]
M is Element of the carrier of ((Y) |^ 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 T_0 () TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
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
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive antisymmetric RelStr
the carrier of (ContMaps (X,(Y))) is non empty set
L is non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of L is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
rng the mapping of L is non empty Element of bool the carrier of (ContMaps (X,(Y)))
bool the carrier of (ContMaps (X,(Y))) is non empty set
"\/" ((rng the mapping of L),((Y) |^ the carrier of X)) is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of ((Y) |^ the carrier of X) is non empty set
C is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty transitive strict directed NetStr over (Y)
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Element of the carrier of (Y)
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 . C is Element of the carrier of (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C), the carrier of (Y):] is non empty set
M is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty transitive strict directed NetStr over (Y)
dom the mapping of L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
dom the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty set
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
M is Element of the carrier of (Y)
the carrier of X --> (Y) is Relation-like the carrier of X -defined {(Y)} -valued Function-like constant non empty V24( the carrier of X) quasi_total RelStr-yielding V395() non-Empty reflexive-yielding TopStruct-yielding Element of bool [: the carrier of X,{(Y)}:]
{(Y)} is non empty set
[: the carrier of X,{(Y)}:] is Relation-like non empty set
bool [: the carrier of X,{(Y)}:] is non empty set
( the carrier of X --> (Y)) . C is non empty reflexive RelStr
M is Element of the carrier of X
M is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty transitive strict directed NetStr over (Y)
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Element of the carrier of (Y)
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 Element of bool [: the carrier of X, the carrier of (Y):]
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 Element of bool [: the carrier of X, the carrier of (Y):]
product ( the carrier of X --> (Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Y))) is non empty set
P is Element of the carrier of ((Y) |^ the carrier of X)
g is Element of the carrier of ((Y) |^ the carrier of X)
i is set
the mapping of L . i is Relation-like Function-like set
g99 is Element of the carrier of (product ( the carrier of X --> (Y)))
t9 is Element of the carrier of (product ( the carrier of X --> (Y)))
j is Element of the carrier of X
( the carrier of X --> (Y)) . j is non empty reflexive RelStr
g99 . j is Element of the carrier of (( the carrier of X --> (Y)) . j)
the carrier of (( the carrier of X --> (Y)) . j) is non empty set
t9 . j is Element of the carrier of (( the carrier of X --> (Y)) . j)
( the carrier of X --> (Y)) . j is non empty reflexive RelStr
g9 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):]
g9 . j is Element of the carrier of (Y)
( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty transitive strict directed NetStr over (Y)
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j), the carrier of (Y):] is non empty set
i is Element of the carrier of L
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) . i is set
M . j is Element of the carrier of (Y)
\\/ ( the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty set
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j)),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty Element of bool the carrier of (Y)
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j)),(Y)) is Element of the carrier of (Y)
c₂₂ is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,c₂₂) is non empty transitive strict directed NetStr over (Y)
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,c₂₂) is Element of the carrier of (Y)
dom the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,j) is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . i is set
g9 . C is Element of the carrier of (Y)
A is Element of the carrier of (product ( the carrier of X --> (Y)))
i is Element of the carrier of (product ( the carrier of X --> (Y)))
P . C is Element of the carrier of (Y)
M is Element of the carrier of (Y)
M is set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) . M is set
M is Element of the carrier of L
the mapping of L . M is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
P 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):]
P . C is Element of the carrier of (Y)
A is Element of the carrier of (Y)
i is Element of the carrier of (Y)
\\/ ( the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C) is non empty set
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,C)),(Y)) is Element of the carrier of (Y)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like T_0 () TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive antisymmetric RelStr
the carrier of (ContMaps (X,(Y))) 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 non empty transitive directed Function-yielding NetStr over ContMaps (X,(Y))
the mapping of L is Relation-like the carrier of L -defined the carrier of (ContMaps (X,(Y))) -valued Function-like non empty V24( the carrier of L) quasi_total Function-yielding V33() Element of bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):]
the carrier of L is non empty set
[: the carrier of L, the carrier of (ContMaps (X,(Y))):] is Relation-like non empty set
bool [: the carrier of L, the carrier of (ContMaps (X,(Y))):] is non empty set
rng the mapping of L is non empty Element of bool the carrier of (ContMaps (X,(Y)))
bool the carrier of (ContMaps (X,(Y))) is non empty set
"\/" ((rng the mapping of L),((Y) |^ the carrier of X)) is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of ((Y) |^ 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 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 (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
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):]
dom the mapping of L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
N 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:]
V is Element of bool the carrier of Y
N " V is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of bool the carrier of X : ex b₂ being Element of the carrier of L ex b₃ being 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):] st
( b₃ = L . b₂ & b₁ = b₃ " V ) } is set
union { b₁ where b₁ is Element of bool the carrier of X : ex b₂ being Element of the carrier of L ex b₃ being 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):] st
( b₃ = L . b₂ & b₁ = b₃ " V ) } is set
M is set
dom N is non empty Element of bool the carrier of X
Funcs ( the carrier of X, the carrier of Y) is functional non empty FUNCTION_DOMAIN of the carrier of X, the carrier of Y
Funcs ( the carrier of L,(Funcs ( the carrier of X, the carrier of Y))) is functional non empty FUNCTION_DOMAIN of the carrier of L, Funcs ( the carrier of X, the carrier of Y)
N . M is set
M is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty transitive strict directed NetStr over (Y)
netmap (( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y)) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):]
the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):] is non empty set
the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) -defined the carrier of (Y) -valued Function-like non empty V24( the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)) quasi_total Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of (Y):]
rng (netmap (( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y))) is non empty Element of bool the carrier of (Y)
N . M is Element of the carrier of Y
sup ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Element of the carrier of (Y)
\\/ ( the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y)) is Element of the carrier of (Y)
rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
"\/" ((rng the mapping of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)),(Y)) is Element of the carrier of (Y)
A is non empty directed Element of bool the carrier of (Y)
"\/" (A,(Y)) is Element of the carrier of (Y)
i is set
dom (netmap (( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y))) is non empty Element of bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M)
bool the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is non empty set
g is set
(netmap (( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y))) . g is set
the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) is Relation-like the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) -defined the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) -valued Element of bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M):]
[: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M):] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M):] is non empty set
RelStr(# the carrier of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M), the InternalRel of ( the carrier of X,(Y),(ContMaps (X,(Y))),L,M) #) is non empty strict transitive 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 transitive RelStr
g9 is Element of the carrier of L
L . g9 is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . g9 is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
g99 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):]
dom g99 is non empty Element of bool the carrier of X
g99 " V is Element of bool the carrier of X
(netmap (( the carrier of X,(Y),(ContMaps (X,(Y))),L,M),(Y))) . g9 is set
commute the mapping of L is Relation-like Function-like Function-yielding V33() set
(commute the mapping of L) . M is Relation-like Function-like set
((commute the mapping of L) . M) . g9 is set
the mapping of L . g9 is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
( the mapping of L . g9) . M is set
M is set
P is Element of bool the carrier of X
i 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):]
A is Element of the carrier of L
L . A is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . A is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
i " V is Element of bool the carrier of X
i 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):]
A is Element of the carrier of L
L . A is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . A is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
i " V is Element of bool the carrier of X
i . M is set
g is Element of the carrier of X
( the carrier of X,(Y),(ContMaps (X,(Y))),L,g) is non empty transitive strict directed NetStr over (Y)
the mapping of L . A is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
g is Element of the carrier of X
i . g is Element of the carrier of (Y)
D . g is Element of the carrier of (Y)
N . g is Element of the carrier of Y
{(N . g)} is non empty compact Element of bool the carrier of Y
g9 is Element of the carrier of (Y)
g99 is Element of the carrier of (Y)
g9 is Element of bool the carrier of Y
Cl g9 is closed Element of bool the carrier of Y
V /\ g9 is Element of bool the carrier of Y
g99 is set
M is set
M is Element of bool the carrier of X
A 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):]
P is Element of the carrier of L
L . P is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . P is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
A " V is Element of bool the carrier of X
bool (bool the carrier of X) is non empty set
M is Element of bool (bool the carrier of X)
M is Element of bool (bool the carrier of X)
P is Element of bool the carrier of X
A is Element of bool the carrier of X
g 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):]
i is Element of the carrier of L
L . i is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . i is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
g " V is Element of bool the carrier of X
g 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):]
i is Element of the carrier of L
L . i is Element of the carrier of (ContMaps (X,(Y)))
the mapping of L . i is Relation-like Function-like Element of the carrier of (ContMaps (X,(Y)))
g " V is Element of bool the carrier of X
g9 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 topology of X is non empty Element of bool (bool the carrier of X)
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
g99 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:]
g99 " V is Element of bool the carrier of X
[#] Y is non empty non proper open closed dense non boundary Element of bool the carrier of Y
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like T_0 () TopStruct
(Y) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Y)) is non empty V213() strict reflexive transitive antisymmetric RelStr
(Y) |^ the carrier of X is non empty V213() strict reflexive transitive antisymmetric RelStr
C is non empty reflexive transitive antisymmetric full SubRelStr of (Y) |^ the carrier of X
the carrier of C is non empty set
bool the carrier of C is non empty set
D is directed Element of bool the carrier of C
"\/" (D,((Y) |^ the carrier of X)) is Element of the carrier of ((Y) |^ the carrier of X)
the carrier of ((Y) |^ the carrier of X) is non empty set
D is non empty directed Element of bool the carrier of C
Net-Str D is non empty reflexive transitive strict directed monotone eventually-directed NetStr over C
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
V is Element of the carrier of X
( the carrier of X,(Y),C,(Net-Str D),V) is non empty transitive strict directed NetStr over (Y)
the mapping of (Net-Str D) is Relation-like the carrier of (Net-Str D) -defined the carrier of C -valued Function-like non empty V24( the carrier of (Net-Str D)) quasi_total Element of bool [: the carrier of (Net-Str D), the carrier of C:]
the carrier of (Net-Str D) is non empty set
[: the carrier of (Net-Str D), the carrier of C:] is Relation-like non empty set
bool [: the carrier of (Net-Str D), the carrier of C:] is non empty set
rng the mapping of (Net-Str D) is non empty Element of bool the carrier of C
"\/" ((rng the mapping of (Net-Str D)),((Y) |^ the carrier of X)) is Element of the carrier of ((Y) |^ the carrier of X)
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 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 (Y) is non empty set
the topology of (Y) is non empty Element of bool (bool the carrier of (Y))
bool the carrier of (Y) is non empty set
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y), the topology of (Y) #) is non empty strict TopSpace-like TopStruct
[: the carrier of X, the carrier of (Y):] is Relation-like non empty set
bool [: the carrier of X, the carrier of (Y):] 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
the InternalRel of C |_2 D is Relation-like D -defined D -valued Element of bool [:D,D:]
[:D,D:] is Relation-like non empty set
bool [:D,D:] is non empty set
the InternalRel of C /\ [:D,D:] is Relation-like the carrier of C -defined the carrier of C -valued set
id the carrier of C is Relation-like the carrier of C -defined the carrier of C -valued Function-like one-to-one non empty V24( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of C:]
(id the carrier of C) | D is Relation-like D -defined the carrier of C -defined the carrier of C -valued Function-like non empty V24(D) quasi_total Element of bool [:D, the carrier of C:]
[:D, the carrier of C:] is Relation-like non empty set
bool [:D, the carrier of C:] is non empty set
NetStr(# D,( the InternalRel of C |_2 D),((id the carrier of C) | D) #) is non empty strict NetStr over C