:: WAYBEL29 semantic presentation

K99() is Element of bool K95()

K95() is set

bool K95() is non empty set

K54() is set

bool K54() is non empty set

bool K99() is non empty set

K246() is non empty strict TopSpace-like TopStruct

the carrier of K246() is non empty set

K96() is set

K97() is set

K98() is set

[:K95(),K95():] is set

bool [:K95(),K95():] is non empty set

K409() is non empty V119() L9()

the carrier of K409() is non empty set

K414() is non empty L9()

K415() is non empty V119() M22(K414())

K416() is non empty V119() V141() V201() M25(K414(),K415())

K418() is non empty V119() V141() V143() V145() L9()

K419() is non empty V119() V141() V201() M22(K418())

{} is set

the Function-like functional empty trivial finite V45() set is Function-like functional empty trivial finite V45() set

1 is non empty set

{{},1} is finite set

[:1,1:] is non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty set

bool [:[:1,1:],1:] is non empty set

K652() is set

{{}} is trivial finite set

K380({{}}) is M19({{}})

[:K380({{}}),{{}}:] is set

bool [:K380({{}}),{{}}:] is non empty set

K39(K380({{}}),{{}}) is set

{1} is trivial finite set

id {{}} is Relation-like {{}} -defined {{}} -valued Function-like one-to-one V24({{}}) quasi_total finite Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is finite set

bool [:{{}},{{}}:] is non empty finite V45() set

RelStr(# {{}},(id {{}}) #) is non empty trivial finite 1 -element strict RelStr

Sierpinski_Space is non empty non trivial strict TopSpace-like T_0 non T_1 injective monotone-convergence TopStruct

0 is Element of K99()

{0,1} is finite set

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

Omega Sierpinski_Space is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete TopRelStr

BoolePoset 1 is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive V379() complemented Boolean RelStr

the carrier of (BoolePoset 1) is non empty set

L is non empty set

S is non empty set

[:L,S:] is non empty set

S is non empty RelStr

S |^ [:L,S:] is non empty V185() strict RelStr

S |^ S is non empty V185() strict RelStr

(S |^ S) |^ L is non empty V185() strict RelStr

SS is non empty V185() SubRelStr of S |^ [:L,S:]

the carrier of SS is functional non empty set

Wy is non empty V185() SubRelStr of (S |^ S) |^ L

the carrier of Wy is functional non empty set

[: the carrier of SS, the carrier of Wy:] is non empty set

bool [: the carrier of SS, the carrier of Wy:] is non empty set

T is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]

T " is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]

[: the carrier of Wy, the carrier of SS:] is non empty set

bool [: the carrier of Wy, the carrier of SS:] is non empty set

rng T is functional Element of bool the carrier of Wy

bool the carrier of Wy is non empty set

T " is Relation-like Function-like set

the carrier of (S |^ S) is functional non empty set

Funcs (L, the carrier of (S |^ S)) is functional non empty FUNCTION_DOMAIN of L, the carrier of (S |^ S)

the carrier of ((S |^ S) |^ L) is functional non empty set

the carrier of S is non empty set

Funcs (S, the carrier of S) is functional non empty FUNCTION_DOMAIN of S, the carrier of S

WY is set

dom (T ") is functional Element of bool the carrier of Wy

[:L,(Funcs (S, the carrier of S)):] is non empty set

bool [:L,(Funcs (S, the carrier of S)):] is non empty set

proj1 (T ") is set

WY is Relation-like Function-like set

(T ") . WY is Relation-like Function-like set

uncurry WY is Relation-like Function-like set

dom T is functional Element of bool the carrier of SS

bool the carrier of SS is non empty set

T1 is set

T . T1 is Relation-like Function-like set

Funcs ([:L,S:], the carrier of S) is functional non empty FUNCTION_DOMAIN of [:L,S:], the carrier of S

the carrier of (S |^ [:L,S:]) is functional non empty set

wy is Relation-like Function-like set

[:[:L,S:], the carrier of S:] is non empty set

bool [:[:L,S:], the carrier of S:] is non empty set

proj1 wy is set

curry wy is Relation-like Function-like set

L is non empty set

S is non empty set

[:L,S:] is non empty set

S is non empty RelStr

S |^ [:L,S:] is non empty V185() strict RelStr

S |^ S is non empty V185() strict RelStr

(S |^ S) |^ L is non empty V185() strict RelStr

SS is non empty V185() SubRelStr of S |^ [:L,S:]

the carrier of SS is functional non empty set

Wy is non empty V185() SubRelStr of (S |^ S) |^ L

the carrier of Wy is functional non empty set

[: the carrier of Wy, the carrier of SS:] is non empty set

bool [: the carrier of Wy, the carrier of SS:] is non empty set

T is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]

T " is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]

[: the carrier of SS, the carrier of Wy:] is non empty set

bool [: the carrier of SS, the carrier of Wy:] is non empty set

the carrier of (S |^ S) is functional non empty set

Funcs (L, the carrier of (S |^ S)) is functional non empty FUNCTION_DOMAIN of L, the carrier of (S |^ S)

the carrier of ((S |^ S) |^ L) is functional non empty set

the carrier of S is non empty set

Funcs (S, the carrier of S) is functional non empty FUNCTION_DOMAIN of S, the carrier of S

rng T is functional Element of bool the carrier of SS

bool the carrier of SS is non empty set

T " is Relation-like Function-like set

Funcs ([:L,S:], the carrier of S) is functional non empty FUNCTION_DOMAIN of [:L,S:], the carrier of S

the carrier of (S |^ [:L,S:]) is functional non empty set

WY is set

dom (T ") is functional Element of bool the carrier of SS

[:[:L,S:], the carrier of S:] is non empty set

bool [:[:L,S:], the carrier of S:] is non empty set

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

dom T1 is Relation-like L -defined S -valued Element of bool [:L,S:]

bool [:L,S:] is non empty set

proj1 T1 is Relation-like set

proj1 WY is set

proj1 (T ") is set

WY is Relation-like Function-like set

(T ") . WY is Relation-like Function-like set

curry WY is Relation-like Function-like set

dom T is functional Element of bool the carrier of Wy

bool the carrier of Wy is non empty set

T1 is set

T . T1 is Relation-like Function-like set

wy is Relation-like Function-like set

[:L,(Funcs (S, the carrier of S)):] is non empty set

bool [:L,(Funcs (S, the carrier of S)):] is non empty set

proj2 wy is set

uncurry wy is Relation-like Function-like set

L is non empty set

S is non empty set

[:L,S:] is non empty set

S is non empty reflexive transitive antisymmetric non void RelStr

S |^ [:L,S:] is non empty V185() strict reflexive transitive antisymmetric non void RelStr

S |^ S is non empty V185() strict reflexive transitive antisymmetric non void RelStr

(S |^ S) |^ L is non empty V185() strict reflexive transitive antisymmetric non void RelStr

SS is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ [:L,S:]

the carrier of SS is functional non empty set

Wy is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of (S |^ S) |^ L

the carrier of Wy is functional non empty set

[: the carrier of SS, the carrier of Wy:] is non empty set

bool [: the carrier of SS, the carrier of Wy:] is non empty set

T is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]

T " is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]

[: the carrier of Wy, the carrier of SS:] is non empty set

bool [: the carrier of Wy, the carrier of SS:] is non empty set

T * (T ") is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]

[: the carrier of Wy, the carrier of Wy:] is non empty set

bool [: the carrier of Wy, the carrier of Wy:] is non empty set

id Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total onto bijective Function-yielding V40() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(Wy) V377(Wy) V378(Wy) Element of bool [: the carrier of Wy, the carrier of Wy:]

id the carrier of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]

(T ") * T is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]

[: the carrier of SS, the carrier of SS:] is non empty set

bool [: the carrier of SS, the carrier of SS:] is non empty set

id SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total onto bijective Function-yielding V40() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(SS) V377(SS) V378(SS) Element of bool [: the carrier of SS, the carrier of SS:]

id the carrier of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]

L is non empty set

S is non empty set

[:L,S:] is non empty set

S is non empty reflexive transitive antisymmetric non void RelStr

S |^ [:L,S:] is non empty V185() strict reflexive transitive antisymmetric non void RelStr

S |^ S is non empty V185() strict reflexive transitive antisymmetric non void RelStr

(S |^ S) |^ L is non empty V185() strict reflexive transitive antisymmetric non void RelStr

SS is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ [:L,S:]

the carrier of SS is functional non empty set

Wy is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of (S |^ S) |^ L

the carrier of Wy is functional non empty set

[: the carrier of Wy, the carrier of SS:] is non empty set

bool [: the carrier of Wy, the carrier of SS:] is non empty set

T is Relation-like the carrier of Wy -defined the carrier of SS -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of SS:]

T " is Relation-like the carrier of SS -defined the carrier of Wy -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of Wy:]

[: the carrier of SS, the carrier of Wy:] is non empty set

bool [: the carrier of SS, the carrier of Wy:] is non empty set

T * (T ") is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]

[: the carrier of SS, the carrier of SS:] is non empty set

bool [: the carrier of SS, the carrier of SS:] is non empty set

id SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total onto bijective Function-yielding V40() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(SS) V377(SS) V378(SS) Element of bool [: the carrier of SS, the carrier of SS:]

id the carrier of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Function-like one-to-one non empty V24( the carrier of SS) quasi_total Function-yielding V40() Element of bool [: the carrier of SS, the carrier of SS:]

(T ") * T is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]

[: the carrier of Wy, the carrier of Wy:] is non empty set

bool [: the carrier of Wy, the carrier of Wy:] is non empty set

id Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total onto bijective Function-yielding V40() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(Wy) V377(Wy) V378(Wy) Element of bool [: the carrier of Wy, the carrier of Wy:]

id the carrier of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Function-like one-to-one non empty V24( the carrier of Wy) quasi_total Function-yielding V40() Element of bool [: the carrier of Wy, the carrier of Wy:]

L is RelStr

the carrier of L is 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 set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

S is RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

S is RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

SS is RelStr

the carrier of SS is set

the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Element of bool [: the carrier of SS, the carrier of SS:]

[: the carrier of SS, the carrier of SS:] is set

bool [: the carrier of SS, the carrier of SS:] is non empty set

RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr

[: the carrier of L, the carrier of S:] is set

bool [: the carrier of L, the carrier of S:] is non empty set

[: the carrier of S, the carrier of SS:] is set

bool [: the carrier of S, the carrier of SS:] is non empty set

Wy is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]

T is Relation-like the carrier of S -defined the carrier of SS -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of SS:]

WY is non empty RelStr

the carrier of WY is non empty set

T1 is non empty RelStr

the carrier of T1 is non empty set

[: the carrier of WY, the carrier of T1:] is non empty set

bool [: the carrier of WY, the carrier of T1:] is non empty set

x is non empty RelStr

the carrier of x is non empty set

y is non empty RelStr

the carrier of y is non empty set

[: the carrier of x, the carrier of y:] is non empty set

bool [: the carrier of x, the carrier of y:] is non empty set

x2 is Element of the carrier of x

u2 is Element of the carrier of x

u1 is Element of the carrier of WY

y1 is Element of the carrier of WY

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

x1 . x2 is Element of the carrier of y

x1 . u2 is Element of the carrier of y

wy is Relation-like the carrier of WY -defined the carrier of T1 -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of T1:]

wy . u1 is Element of the carrier of T1

wy . y1 is Element of the carrier of T1

rng wy is Element of bool the carrier of T1

bool the carrier of T1 is non empty set

L is RelStr

the carrier of L is set

S is RelStr

the carrier of S is set

[: the carrier of L, the carrier of S:] is set

bool [: the carrier of L, the carrier of S:] is non empty set

S is RelStr

the carrier of S is set

[: the carrier of S, the carrier of S:] is set

bool [: the carrier of S, the carrier of S:] is non empty set

[: the carrier of L, the carrier of S:] is set

bool [: the carrier of L, the carrier of S:] is non empty set

SS is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]

Wy is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]

Wy * SS is Relation-like the carrier of L -defined the carrier of S -valued Function-like Element of bool [: the carrier of L, the carrier of S:]

T is Relation-like the carrier of L -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of S:]

WY is non empty RelStr

the carrier of WY is non empty set

T1 is non empty RelStr

the carrier of T1 is non empty set

[: the carrier of WY, the carrier of T1:] is non empty set

bool [: the carrier of WY, the carrier of T1:] is non empty set

wy is non empty RelStr

the carrier of wy is non empty set

[: the carrier of T1, the carrier of wy:] is non empty set

bool [: the carrier of T1, the carrier of wy:] is non empty set

[: the carrier of T1, the carrier of WY:] is non empty set

bool [: the carrier of T1, the carrier of WY:] is non empty set

x is Relation-like the carrier of WY -defined the carrier of T1 -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of T1:]

x " is Relation-like Function-like set

x1 is Relation-like the carrier of T1 -defined the carrier of WY -valued Function-like non empty V24( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of WY:]

[: the carrier of wy, the carrier of T1:] is non empty set

bool [: the carrier of wy, the carrier of T1:] is non empty set

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

y " is Relation-like Function-like set

x2 is Relation-like the carrier of wy -defined the carrier of T1 -valued Function-like non empty V24( the carrier of wy) quasi_total Element of bool [: the carrier of wy, the carrier of T1:]

y * x is Relation-like the carrier of WY -defined the carrier of wy -valued Function-like non empty V24( the carrier of WY) quasi_total Element of bool [: the carrier of WY, the carrier of wy:]

[: the carrier of WY, the carrier of wy:] is non empty set

bool [: the carrier of WY, the carrier of wy:] is non empty set

x1 * x2 is Relation-like the carrier of wy -defined the carrier of WY -valued Function-like non empty V24( the carrier of wy) quasi_total Element of bool [: the carrier of wy, the carrier of WY:]

[: the carrier of wy, the carrier of WY:] is non empty set

bool [: the carrier of wy, the carrier of WY:] is non empty set

(y * x) " is Relation-like Function-like set

L is TopSpace-like TopStruct

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

S is TopSpace-like TopStruct

the carrier of S is set

the topology of S is non empty Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

S is TopSpace-like TopStruct

the carrier of S is set

the topology of S is non empty Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

SS is TopSpace-like TopStruct

the carrier of SS is set

the topology of SS is non empty Element of bool (bool the carrier of SS)

bool the carrier of SS is non empty set

bool (bool the carrier of SS) is non empty set

TopStruct(# the carrier of SS, the topology of SS #) is strict TopSpace-like TopStruct

[:L,S:] is strict TopSpace-like TopStruct

[:S,SS:] is strict TopSpace-like TopStruct

the carrier of [:S,SS:] is set

bool the carrier of [:S,SS:] is non empty set

bool (bool the carrier of [:S,SS:]) is non empty set

{ [:b

{ (union b

the carrier of [:L,S:] is set

[: the carrier of L, the carrier of S:] is set

the topology of [:L,S:] is non empty Element of bool (bool the carrier of [:L,S:])

bool the carrier of [:L,S:] is non empty set

bool (bool the carrier of [:L,S:]) is non empty set

the topology of [:S,SS:] is non empty Element of bool (bool the carrier of [:S,SS:])

L is non empty TopSpace-like TopStruct

the carrier of L is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopRelStr

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

the carrier of (ContMaps (L,S)) is functional non empty set

bool the carrier of (ContMaps (L,S)) is non empty set

S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr

the carrier of S is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

S is functional non empty directed Element of bool the carrier of (ContMaps (L,S))

"\/" (S,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

the carrier of (S |^ the carrier of L) is functional non empty set

Funcs ( the carrier of L, the carrier of S) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of S

bool the carrier of (S |^ the carrier of L) is non empty set

bool the carrier of S is non empty set

WY is Element of bool the carrier of S

T1 is set

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

Wy " WY is Element of bool the carrier of L

bool the carrier of L is non empty set

Wy . T1 is set

the carrier of L --> S is Relation-like the carrier of L -defined Function-like constant non empty V24( the carrier of L) V326() RelStr-yielding non-Empty reflexive-yielding TopStruct-yielding Poset-yielding set

product ( the carrier of L --> S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

wy is Element of the carrier of L

( the carrier of L --> S) . wy is non empty reflexive transitive antisymmetric non void RelStr

T is functional non empty directed Element of bool the carrier of (S |^ the carrier of L)

pi (T,wy) is non empty Element of bool the carrier of S

"\/" (T,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

("\/" (T,(S |^ the carrier of L))) . wy is Element of the carrier of S

"\/" ((pi (T,wy)),S) is Element of the carrier of S

x is set

y is Relation-like Function-like set

y . wy is set

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

x1 " WY is Element of bool the carrier of L

[#] S is non empty non proper open closed dense non boundary lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of S

x2 is Element of bool the carrier of L

dom Wy is Element of bool the carrier of L

u2 is set

x1 . u2 is set

u1 is Element of the carrier of L

( the carrier of L --> S) . u1 is non empty reflexive transitive antisymmetric non void RelStr

pi (T,u1) is non empty Element of bool the carrier of S

Wy . u1 is Element of the carrier of S

"\/" ((pi (T,u1)),S) is Element of the carrier of S

x1 . u1 is Element of the carrier of S

dom x1 is Element of bool the carrier of L

wy is Element of bool the carrier of L

L is non empty TopSpace-like TopStruct

the carrier of L is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopRelStr

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr

S is non empty V185() reflexive transitive antisymmetric full non void SubRelStr of S |^ the carrier of L

the carrier of S is functional non empty set

bool the carrier of S is non empty set

SS is functional directed Element of bool the carrier of S

"\/" (SS,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

the carrier of (S |^ the carrier of L) is functional non empty set

Wy is functional non empty directed Element of bool the carrier of S

"\/" (Wy,(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

the carrier of S is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

L is TopStruct

the carrier of L is set

the topology of L is Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

TopStruct(# the carrier of L, the topology of L #) is strict TopStruct

S is TopStruct

the carrier of S is set

the topology of S is Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopStruct(# the carrier of S, the topology of S #) is strict TopStruct

S is non empty TopRelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

the topology of S is Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) is strict TopRelStr

SS is non empty TopRelStr

the carrier of SS is non empty set

the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued Element of bool [: the carrier of SS, the carrier of SS:]

[: the carrier of SS, the carrier of SS:] is non empty set

bool [: the carrier of SS, the carrier of SS:] is non empty set

the topology of SS is Element of bool (bool the carrier of SS)

bool the carrier of SS is non empty set

bool (bool the carrier of SS) is non empty set

TopRelStr(# the carrier of SS, the InternalRel of SS, the topology of SS #) is strict TopRelStr

ContMaps (L,S) is strict RelStr

ContMaps (S,SS) is strict RelStr

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr

S |^ the carrier of L is non empty V185() strict RelStr

SS |^ the carrier of S is non empty V185() strict RelStr

the carrier of (ContMaps (L,S)) is set

the carrier of (ContMaps (S,SS)) is set

WY is set

[: the carrier of L, the carrier of S:] is set

bool [: the carrier of L, the carrier of S:] is non empty set

T1 is Relation-like the carrier of L -defined the carrier of S -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]

[: the carrier of S, the carrier of SS:] is set

bool [: the carrier of S, the carrier of SS:] is non empty set

wy is Relation-like the carrier of S -defined the carrier of SS -valued Function-like V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of SS:]

x is Element of bool the carrier of SS

wy " x is Element of bool the carrier of S

[#] SS is non empty non proper dense lower upper Element of bool the carrier of SS

([#] SS) \ x is Element of bool the carrier of SS

[#] S is non empty non proper dense lower upper Element of bool the carrier of S

y is Element of bool the carrier of S

([#] S) \ y is Element of bool the carrier of S

T1 " y is Element of bool the carrier of L

[#] L is non proper dense Element of bool the carrier of L

([#] L) \ (T1 " y) is Element of bool the carrier of L

([#] L) \ (wy " x) is Element of bool the carrier of L

[#] S is non proper dense Element of bool the carrier of S

([#] S) \ (wy " x) is Element of bool the carrier of S

WY is set

[: the carrier of S, the carrier of SS:] is set

bool [: the carrier of S, the carrier of SS:] is non empty set

T1 is Relation-like the carrier of S -defined the carrier of SS -valued Function-like V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of SS:]

[: the carrier of L, the carrier of S:] is set

bool [: the carrier of L, the carrier of S:] is non empty set

wy is Relation-like the carrier of L -defined the carrier of S -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]

x is Element of bool the carrier of S

wy " x is Element of bool the carrier of L

[#] S is non empty non proper dense lower upper Element of bool the carrier of S

([#] S) \ x is Element of bool the carrier of S

y is Element of bool the carrier of SS

([#] S) \ y is Element of bool the carrier of S

[#] SS is non empty non proper dense lower upper Element of bool the carrier of SS

([#] SS) \ y is Element of bool the carrier of SS

T1 " y is Element of bool the carrier of S

[#] S is non proper dense Element of bool the carrier of S

([#] S) \ (T1 " y) is Element of bool the carrier of S

([#] S) \ (wy " x) is Element of bool the carrier of S

[#] L is non proper dense Element of bool the carrier of L

([#] L) \ (wy " x) is Element of bool the carrier of L

T is full SubRelStr of S |^ the carrier of L

the carrier of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

Wy is full SubRelStr of S |^ the carrier of L

the carrier of Wy is set

the InternalRel of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued Element of bool [: the carrier of Wy, the carrier of Wy:]

[: the carrier of Wy, the carrier of Wy:] is set

bool [: the carrier of Wy, the carrier of Wy:] is non empty set

RelStr(# the carrier of Wy, the InternalRel of Wy #) is strict RelStr

L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete TopRelStr

the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete RelStr is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete RelStr

the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete RelStr is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete satisfying_axiom_of_approximation continuous non void with_suprema with_infima complete RelStr

L is non empty TopSpace-like TopStruct

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopRelStr

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

the carrier of L is non empty set

S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric up-complete non void RelStr

L is non empty set

S is Relation-like L -defined Function-like V24(L) V326() RelStr-yielding non-Empty reflexive-yielding Poset-yielding set

product S is non empty V185() strict reflexive transitive antisymmetric non void RelStr

the carrier of (product S) is functional non empty set

bool the carrier of (product S) is non empty set

Wy is Element of L

S . Wy is non empty reflexive transitive antisymmetric non void RelStr

S . Wy is non empty reflexive non void RelStr

SS is functional non empty directed Element of bool the carrier of (product S)

pi (SS,Wy) is non empty Element of bool the carrier of (S . Wy)

the carrier of (S . Wy) is non empty set

bool the carrier of (S . Wy) is non empty set

L is non empty set

bool L is non empty set

S is Relation-like L -defined Function-like V24(L) V326() RelStr-yielding non-Empty reflexive-yielding Poset-yielding set

product S is non empty V185() strict reflexive transitive antisymmetric non void RelStr

the carrier of (product S) is functional non empty set

Wy is Relation-like Function-like Element of the carrier of (product S)

T is Relation-like Function-like Element of the carrier of (product S)

WY is Element of L

S . WY is non empty reflexive non void RelStr

Wy . WY is Element of the carrier of (S . WY)

the carrier of (S . WY) is non empty set

T . WY is Element of the carrier of (S . WY)

S . WY is non empty reflexive transitive antisymmetric non void RelStr

the carrier of (S . WY) is non empty set

bool the carrier of (S . WY) is non empty set

T1 is non empty directed Element of bool the carrier of (S . WY)

"\/" (T1,(S . WY)) is Element of the carrier of (S . WY)

"\/" (T1,(S . WY)) is Element of the carrier of (S . WY)

the Element of T1 is Element of T1

{ (T +* (WY,b

proj1 T is set

x1 is set

x2 is Element of the carrier of (S . WY)

T +* (WY,x2) is Relation-like Function-like set

u2 is Element of L

(T +* (WY,x2)) . u2 is set

T . u2 is Element of the carrier of (S . u2)

S . u2 is non empty reflexive non void RelStr

the carrier of (S . u2) is non empty set

S . u2 is non empty reflexive transitive antisymmetric non void RelStr

the carrier of (S . u2) is non empty set

proj1 (T +* (WY,x2)) is set

bool the carrier of (product S) is non empty set

y is Element of the carrier of (S . WY)

T +* (WY,y) is Relation-like Function-like set

x1 is functional Element of bool the carrier of (product S)

x2 is functional non empty Element of bool the carrier of (product S)

u2 is Relation-like Function-like Element of the carrier of (product S)

u1 is Relation-like Function-like Element of the carrier of (product S)

y1 is Element of the carrier of (S . WY)

T +* (WY,y1) is Relation-like Function-like set

y2 is Element of the carrier of (S . WY)

T +* (WY,y2) is Relation-like Function-like set

y1 is Element of the carrier of (S . WY)

T +* (WY,y1) is Relation-like Function-like set

y2 is Relation-like Function-like Element of the carrier of (product S)

v2 is Element of L

y2 . v2 is Element of the carrier of (S . v2)

S . v2 is non empty reflexive non void RelStr

the carrier of (S . v2) is non empty set

u2 . v2 is Element of the carrier of (S . v2)

T . v2 is Element of the carrier of (S . v2)

v2 is Element of L

y2 . v2 is Element of the carrier of (S . v2)

S . v2 is non empty reflexive non void RelStr

the carrier of (S . v2) is non empty set

u1 . v2 is Element of the carrier of (S . v2)

T . v2 is Element of the carrier of (S . v2)

u2 is functional non empty directed Element of bool the carrier of (product S)

pi (u2,WY) is non empty Element of bool the carrier of (S . WY)

bool the carrier of (S . WY) is non empty set

u1 is set

y1 is Element of the carrier of (S . WY)

T +* (WY,y1) is Relation-like Function-like set

(T +* (WY,y1)) . WY is set

u1 is Element of L

S . u1 is non empty reflexive transitive antisymmetric non void RelStr

"\/" ((pi (u2,WY)),(S . WY)) is Element of the carrier of (S . WY)

SS is non empty reflexive transitive antisymmetric up-complete non void RelStr

"\/" (u2,(product S)) is Relation-like Function-like Element of the carrier of (product S)

("\/" (u2,(product S))) . u1 is Element of the carrier of (S . u1)

S . u1 is non empty reflexive non void RelStr

the carrier of (S . u1) is non empty set

pi (u2,u1) is non empty Element of bool the carrier of (S . u1)

bool the carrier of (S . u1) is non empty set

"\/" ((pi (u2,u1)),(S . u1)) is Element of the carrier of (S . u1)

(T +* (WY,y)) . u1 is set

T . u1 is Element of the carrier of (S . u1)

u1 is Relation-like Function-like Element of the carrier of (product S)

y1 is Element of the carrier of (S . WY)

T +* (WY,y1) is Relation-like Function-like set

u1 . WY is Element of the carrier of (S . WY)

{ b

T1 is set

wy is Element of L

Wy . wy is Element of the carrier of (S . wy)

S . wy is non empty reflexive non void RelStr

the carrier of (S . wy) is non empty set

S . wy is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . wy) is Element of the carrier of (S . wy)

the carrier of (S . wy) is non empty set

"\/" ({},(S . wy)) is Element of the carrier of (S . wy)

wy is Relation-like L -defined Function-like V24(L) set

x is Element of L

wy . x is set

S . x is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . x) is Element of the carrier of (S . x)

the carrier of (S . x) is non empty set

"\/" ({},(S . x)) is Element of the carrier of (S . x)

dom wy is Element of bool L

x is Relation-like Function-like Element of the carrier of (product S)

{ (x +* (T | b

x1 is set

x2 is finite Element of bool L

T | x2 is Relation-like Function-like finite set

x +* (T | x2) is Relation-like Function-like set

proj1 T is set

proj1 (T | x2) is finite set

u2 is Element of L

(x +* (T | x2)) . u2 is set

x . u2 is Element of the carrier of (S . u2)

S . u2 is non empty reflexive non void RelStr

the carrier of (S . u2) is non empty set

(T | x2) . u2 is set

T . u2 is Element of the carrier of (S . u2)

S . u2 is non empty reflexive transitive antisymmetric non void RelStr

the carrier of (S . u2) is non empty set

L \/ (proj1 (T | x2)) is set

proj1 (x +* (T | x2)) is set

bool the carrier of (product S) is non empty set

{} L is Function-like functional empty trivial proper finite V45() Element of bool L

T | ({} L) is Relation-like Function-like finite set

x +* (T | ({} L)) is Relation-like Function-like set

x1 is functional Element of bool the carrier of (product S)

x2 is functional non empty Element of bool the carrier of (product S)

u2 is Relation-like Function-like Element of the carrier of (product S)

u1 is Relation-like Function-like Element of the carrier of (product S)

y1 is finite Element of bool L

T | y1 is Relation-like Function-like finite set

x +* (T | y1) is Relation-like Function-like set

y2 is finite Element of bool L

T | y2 is Relation-like Function-like finite set

x +* (T | y2) is Relation-like Function-like set

y1 \/ y2 is finite Element of bool L

y1 is finite Element of bool L

T | y1 is Relation-like Function-like finite set

x +* (T | y1) is Relation-like Function-like set

y2 is Relation-like Function-like Element of the carrier of (product S)

proj1 T is set

proj1 (T | y1) is finite set

proj1 (T | y1) is finite set

v2 is Element of L

x . v2 is Element of the carrier of (S . v2)

S . v2 is non empty reflexive non void RelStr

the carrier of (S . v2) is non empty set

S . v2 is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . v2) is Element of the carrier of (S . v2)

the carrier of (S . v2) is non empty set

"\/" ({},(S . v2)) is Element of the carrier of (S . v2)

T . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

(T | y1) . v2 is set

u2 . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

u2 . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

(T | y1) . v2 is set

u2 . v2 is Element of the carrier of (S . v2)

(T | y1) . v2 is set

proj1 (T | y2) is finite set

v2 is Element of L

x . v2 is Element of the carrier of (S . v2)

S . v2 is non empty reflexive non void RelStr

the carrier of (S . v2) is non empty set

S . v2 is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . v2) is Element of the carrier of (S . v2)

the carrier of (S . v2) is non empty set

"\/" ({},(S . v2)) is Element of the carrier of (S . v2)

T . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

(T | y1) . v2 is set

u1 . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

u1 . v2 is Element of the carrier of (S . v2)

y2 . v2 is Element of the carrier of (S . v2)

(T | y1) . v2 is set

u1 . v2 is Element of the carrier of (S . v2)

(T | y2) . v2 is set

u1 is Element of L

{u1} is trivial finite set

y1 is finite Element of bool L

T | y1 is Relation-like Function-like finite set

x +* (T | y1) is Relation-like Function-like set

u2 is functional non empty directed Element of bool the carrier of (product S)

SS is non empty reflexive transitive antisymmetric up-complete non void RelStr

"\/" (u2,(product S)) is Relation-like Function-like Element of the carrier of (product S)

y2 is Relation-like Function-like Element of the carrier of (product S)

proj1 T is set

proj1 (T | y1) is finite set

(T | y1) . u1 is set

T . u1 is Element of the carrier of (S . u1)

S . u1 is non empty reflexive non void RelStr

the carrier of (S . u1) is non empty set

y2 . u1 is Element of the carrier of (S . u1)

("\/" (u2,(product S))) . u1 is Element of the carrier of (S . u1)

u1 is Relation-like Function-like Element of the carrier of (product S)

y1 is finite Element of bool L

T | y1 is Relation-like Function-like finite set

x +* (T | y1) is Relation-like Function-like set

T1 is Element of bool L

proj1 (T | y1) is finite set

y2 is set

y1 is Element of L

Wy . y1 is Element of the carrier of (S . y1)

S . y1 is non empty reflexive non void RelStr

the carrier of (S . y1) is non empty set

S . y1 is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . y1) is Element of the carrier of (S . y1)

the carrier of (S . y1) is non empty set

"\/" ({},(S . y1)) is Element of the carrier of (S . y1)

u1 . y1 is Element of the carrier of (S . y1)

x . y1 is Element of the carrier of (S . y1)

y2 is finite Element of bool L

y1 is finite Element of bool L

y2 is Element of L

Wy . y2 is Element of the carrier of (S . y2)

S . y2 is non empty reflexive non void RelStr

the carrier of (S . y2) is non empty set

S . y2 is non empty reflexive transitive antisymmetric non void RelStr

Bottom (S . y2) is Element of the carrier of (S . y2)

the carrier of (S . y2) is non empty set

"\/" ({},(S . y2)) is Element of the carrier of (S . y2)

WY is finite Element of bool L

T1 is functional non empty directed Element of bool the carrier of (product S)

"\/" (T1,(product S)) is Relation-like Function-like Element of the carrier of (product S)

wy is set

x is Element of L

S . x is non empty reflexive non void RelStr

pi (T1,x) is non empty Element of bool the carrier of (S . x)

the carrier of (S . x) is non empty set

bool the carrier of (S . x) is non empty set

S . x is non empty reflexive transitive antisymmetric non void RelStr

the carrier of (S . x) is non empty set

y is Element of the carrier of (S . x)

x1 is Element of the carrier of (S . x)

x2 is Relation-like Function-like set

x2 . x is set

u2 is Relation-like Function-like set

u2 . x is set

u1 is Relation-like Function-like Element of the carrier of (product S)

y1 is Relation-like Function-like Element of the carrier of (product S)

y2 is Relation-like Function-like Element of the carrier of (product S)

y2 . x is Element of the carrier of (S . x)

("\/" (T1,(product S))) . x is Element of the carrier of (S . x)

"\/" ((pi (T1,x)),(S . x)) is Element of the carrier of (S . x)

Wy . x is Element of the carrier of (S . x)

T . x is Element of the carrier of (S . x)

S . x is non empty reflexive transitive antisymmetric non void RelStr

the carrier of (S . x) is non empty set

y is Element of the carrier of (S . x)

x1 is Relation-like Function-like set

x1 . x is set

x2 is set

u2 is set

wy is Relation-like Function-like set

proj1 wy is set

proj2 wy is set

bool T1 is non empty set

x is functional finite Element of bool T1

y is Relation-like Function-like Element of the carrier of (product S)

x1 is Element of L

S . x1 is non empty reflexive transitive antisymmetric non void RelStr

wy . x1 is set

x2 is Element of L

u2 is Relation-like Function-like Element of the carrier of (product S)

S . x2 is non empty reflexive non void RelStr

Wy . x2 is Element of the carrier of (S . x2)

the carrier of (S . x2) is non empty set

u2 . x2 is Element of the carrier of (S . x2)

S . x1 is non empty reflexive non void RelStr

u2 . x1 is Element of the carrier of (S . x1)

the carrier of (S . x1) is non empty set

y . x1 is Element of the carrier of (S . x1)

Wy . x1 is Element of the carrier of (S . x1)

Wy . x1 is Element of the carrier of (S . x1)

S . x1 is non empty reflexive non void RelStr

the carrier of (S . x1) is non empty set

Bottom (S . x1) is Element of the carrier of (S . x1)

the carrier of (S . x1) is non empty set

"\/" ({},(S . x1)) is Element of the carrier of (S . x1)

y . x1 is Element of the carrier of (S . x1)

L is set

S is non empty reflexive antisymmetric lower-bounded non void RelStr

S |^ L is non empty V185() strict reflexive antisymmetric non void RelStr

the carrier of S is non empty set

Bottom S is Element of the carrier of S

"\/" ({},S) is Element of the carrier of S

L --> (Bottom S) is Relation-like L -defined the carrier of S -valued Function-like constant V24(L) quasi_total Element of bool [:L, the carrier of S:]

[:L, the carrier of S:] is set

bool [:L, the carrier of S:] is non empty set

rng (L --> (Bottom S)) is trivial finite Element of bool the carrier of S

bool the carrier of S is non empty set

the carrier of (S |^ L) is functional non empty set

Funcs (L, the carrier of S) is functional non empty FUNCTION_DOMAIN of L, the carrier of S

dom (L --> (Bottom S)) is Element of bool L

bool L is non empty set

S is Relation-like Function-like Element of the carrier of (S |^ L)

SS is Relation-like Function-like Element of the carrier of (S |^ L)

Wy is non empty set

S |^ Wy is non empty V185() strict reflexive antisymmetric non void RelStr

the carrier of (S |^ Wy) is functional non empty set

T is Relation-like Function-like Element of the carrier of (S |^ Wy)

T1 is Element of Wy

T . T1 is Element of the carrier of S

WY is Relation-like Function-like Element of the carrier of (S |^ Wy)

WY . T1 is Element of the carrier of S

L is non empty TopSpace-like TopStruct

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded non void TopRelStr

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

the carrier of (ContMaps (L,S)) is functional non empty set

Bottom S is Element of the carrier of S

the carrier of S is non empty set

"\/" ({},S) is Element of the carrier of S

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

the carrier of L is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

the carrier of L --> (Bottom S) is Relation-like the carrier of L -defined the carrier of S -valued Function-like constant non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of S:]

S is Relation-like Function-like Element of the carrier of (ContMaps (L,S))

SS is Relation-like Function-like Element of the carrier of (ContMaps (L,S))

S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric lower-bounded non void RelStr

the carrier of (S |^ the carrier of L) is functional non empty set

Omega L is non empty TopSpace-like reflexive transitive strict non void TopRelStr

the carrier of (Omega L) is non empty set

the topology of (Omega L) is non empty Element of bool (bool the carrier of (Omega L))

bool the carrier of (Omega L) is non empty set

bool (bool the carrier of (Omega L)) is non empty set

TopStruct(# the carrier of (Omega L), the topology of (Omega L) #) is non empty strict TopSpace-like TopStruct

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

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

[: the carrier of (Omega L), the carrier of S:] is non empty set

bool [: the carrier of (Omega L), the carrier of S:] is non empty set

the carrier of (Omega L) --> (Bottom S) is Relation-like the carrier of (Omega L) -defined the carrier of S -valued Function-like constant non empty V24( the carrier of (Omega L)) quasi_total quasi_total monotone Element of bool [: the carrier of (Omega L), the carrier of S:]

Bottom (S |^ the carrier of L) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

"\/" ({},(S |^ the carrier of L)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

Wy is Relation-like Function-like Element of the carrier of (S |^ the carrier of L)

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

S is non empty reflexive transitive antisymmetric non void TopAugmentation of L

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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

S is non empty reflexive transitive antisymmetric up-complete non void TopAugmentation of L

[#] S is non empty non proper dense lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is non empty set

the topology of S is Element of bool (bool the carrier of S)

bool (bool the carrier of S) is non empty set

S is Element of bool (bool the carrier of S)

union S is Element of bool the carrier of S

SS is non empty directed Element of bool the carrier of S

"\/" (SS,S) is Element of the carrier of S

Wy is set

T is Element of bool the carrier of S

WY is set

SS is Element of bool the carrier of S

S is Element of bool the carrier of S

SS is Element of bool the carrier of S

S /\ SS is Element of bool the carrier of S

T is Element of bool the carrier of S

Wy is Element of bool the carrier of S

WY is non empty directed Element of bool the carrier of S

"\/" (WY,S) is Element of the carrier of S

T1 is set

wy is set

x is Element of the carrier of S

y is Element of the carrier of S

x1 is Element of the carrier of S

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

{ b

bool the carrier of L is non empty Element of bool (bool the carrier of L)

bool (bool the carrier of L) is non empty set

S is set

SS is Element of bool the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

bool [: the carrier of L, the carrier of L:] is non empty set

S is Element of bool (bool the carrier of L)

TopRelStr(# the carrier of L, the InternalRel of L,S #) is strict TopRelStr

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) is set

the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,S #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):]

[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):] is set

bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #):] is non empty set

RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,S #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,S #) #) is strict RelStr

Wy is non empty reflexive transitive antisymmetric up-complete non void TopAugmentation of L

the carrier of Wy is non empty set

bool the carrier of Wy is non empty set

T is Element of bool the carrier of Wy

WY is Element of bool the carrier of L

WY is Element of bool the carrier of L

the topology of Wy is Element of bool (bool the carrier of Wy)

bool (bool the carrier of Wy) is non empty set

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopAugmentation of L

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopAugmentation of L

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict 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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

SS is set

Wy is open upper inaccessible_by_directed_joins Element of bool the carrier of S

T is Element of bool the carrier of S

SS is set

Wy is open upper inaccessible_by_directed_joins Element of bool the carrier of S

T is Element of bool the carrier of S

L is non empty reflexive antisymmetric up-complete non void TopRelStr

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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

bool [: the carrier of L, the carrier of L:] is non empty 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

TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is strict TopRelStr

S is non empty reflexive antisymmetric up-complete non void TopRelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

the topology of S is Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) is strict TopRelStr

S is Element of bool the carrier of S

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

SS is Element of bool the carrier of L

SS is Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict 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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

L is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott non void TopRelStr

(L) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty set

bool [: the carrier of L, the carrier of L:] is non empty set

the topology of L is non empty Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is strict TopRelStr

the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is set

the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):]

[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):] is set

bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #):] is non empty set

RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) #) is strict RelStr

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

S is non empty reflexive transitive antisymmetric up-complete non void TopAugmentation of L

L is non empty reflexive transitive antisymmetric up-complete non void 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 non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

S is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

(L) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

(S) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of S

the carrier of (S) is non empty set

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

RelStr(# the carrier of (S), the InternalRel of (S) #) is strict 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 non empty Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is 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 strict RelStr

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of L is non empty set

S is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of S is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

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

(L) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

the carrier of (L) is non empty set

(S) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of S

the carrier of (S) is non empty set

[: the carrier of (L), the carrier of (S):] is non empty set

bool [: the carrier of (L), the carrier of (S):] is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is 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 strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of L is non empty set

S is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of S is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

(L) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

(S) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of S

S is Relation-like the carrier of L -defined the carrier of S -valued Function-like non empty V24( the carrier of L) quasi_total directed-sups-preserving Element of bool [: the carrier of L, the carrier of S:]

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

the carrier of (L) is non empty set

the carrier of (S) is non empty set

[: the carrier of (L), the carrier of (S):] is non empty set

bool [: the carrier of (L), the carrier of (S):] is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is 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 strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

L is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of L is non empty set

S is non empty reflexive transitive antisymmetric up-complete non void RelStr

the carrier of S is non empty set

[: the carrier of L, the carrier of S:] is non empty set

bool [: the carrier of L, the carrier of S:] is non empty set

(L) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of L

(S) is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict Scott non void TopAugmentation of S

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

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

the carrier of (L) is non empty set

the carrier of (S) is non empty set

[: the carrier of (L), the carrier of (S):] is non empty set

bool [: the carrier of (L), the carrier of (S):] is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued non empty Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is 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 strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued non empty Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is 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 strict RelStr

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued non empty Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

RelStr(# the carrier of (S), the InternalRel of (S) #) is strict RelStr

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued non empty Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr

L is non empty TopSpace-like TopStruct

S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void with_suprema with_infima complete TopRelStr

oContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric non void RelStr

ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non