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 .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : a1 in b1 } is set
"\/" ( { (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : a1 in b1 } ,Y) is Element of the carrier of Y
D is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
N is Relation-like the carrier of D -defined the carrier of Y -valued Function-like non empty V24( the carrier of D) quasi_total Element of bool [: the carrier of D, the carrier of Y:]
N | the carrier of L is Relation-like the carrier of L -defined the carrier of D -defined the carrier of Y -valued Function-like Element of bool [: the carrier of D, the carrier of Y:]
dom C is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
bool the carrier of Y is non empty set
V is Element of bool the carrier of Y
N " V is Element of bool the carrier of D
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 .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } is set
A is set
i is open Element of bool the carrier of D
i /\ the carrier of L is Element of bool the carrier of D
C .: (i /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (i /\ the carrier of L)) is Element of the carrier of Y
[#] D is non empty non proper open closed dense non boundary Element of bool the carrier of D
([#] D) /\ the carrier of L is Element of bool the carrier of D
C .: (([#] D) /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (([#] D) /\ the carrier of L)) is Element of the carrier of Y
A is Element of bool the carrier of Y
i is Element of the carrier of Y
g is Element of the carrier of Y
g9 is open Element of bool the carrier of D
g9 /\ the carrier of L is Element of bool the carrier of D
C .: (g9 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g9 /\ the carrier of L)) is Element of the carrier of Y
g99 is open Element of bool the carrier of D
g99 /\ the carrier of L is Element of bool the carrier of D
C .: (g99 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g99 /\ the carrier of L)) is Element of the carrier of Y
g9 /\ g99 is open Element of bool the carrier of D
(g9 /\ g99) /\ the carrier of L is Element of bool the carrier of D
C .: ((g9 /\ g99) /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: ((g9 /\ g99) /\ the carrier of L)) is Element of the carrier of Y
N . M is Element of the carrier of Y
"\/" (A,Y) is Element of the carrier of Y
i is set
g is open Element of bool the carrier of D
g /\ the carrier of L is Element of bool the carrier of D
C .: (g /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g /\ the carrier of L)) is Element of the carrier of Y
g99 is set
t9 is Element of the carrier of D
N . t9 is Element of the carrier of Y
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : t9 in b1 } is set
"\/" ( { (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : t9 in b1 } ,Y) is Element of the carrier of Y
g9 is Element of the carrier of Y
M is Element of bool the carrier of D
M is set
(N | the carrier of L) . M is set
C . M is set
M is Element of the carrier of L
M is Element of the carrier of D
{ (inf (C .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } is set
A is set
i is open Element of bool the carrier of D
i /\ the carrier of L is Element of bool the carrier of D
C .: (i /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (i /\ the carrier of L)) is Element of the carrier of Y
A is Element of bool the carrier of Y
C . M is Element of the carrier of Y
i is Element of the carrier of Y
g is open Element of bool the carrier of D
g /\ the carrier of L is Element of bool the carrier of D
C .: (g /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g /\ the carrier of L)) is Element of the carrier of Y
i is Element of the carrier of Y
g is open Element of bool the carrier of L
C .: g is Element of bool the carrier of Y
inf (C .: g) is Element of the carrier of Y
the topology of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
the topology of D is non empty Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
[#] L is non empty non proper open closed dense non boundary Element of bool the carrier of L
g9 is Element of bool the carrier of D
g9 /\ ([#] L) is Element of bool the carrier of L
g99 is open Element of bool the carrier of D
g99 /\ the carrier of L is Element of bool the carrier of D
C .: (g99 /\ the carrier of L) is Element of bool the carrier of Y
inf (C .: (g99 /\ the carrier of L)) is Element of the carrier of Y
waybelow (C . M) is non empty directed lower Element of bool the carrier of Y
g is Element of the carrier of Y
wayabove g is upper Element of bool the carrier of Y
C " (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 .: (b1 /\ the carrier of L))) where b1 is open Element of bool the carrier of D : M in b1 } ,Y) is Element of the carrier of Y
[#] 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