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

"\/" ( { (inf (C .: (b

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

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

"\/" ( { (inf (C .: (b

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

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

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