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
{ [:b1,b2:] where b1 is Element of bool the carrier of S, b2 is Element of bool the carrier of SS : ( b1 in the topology of S & b2 in the topology of SS ) } is set
{ (union b1) where b1 is Element of bool (bool the carrier of [:S,SS:]) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of S, b3 is Element of bool the carrier of SS : ( b1 in the topology of S & b2 in the topology of SS ) } } is set
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,b1)) where b1 is Element of the carrier of (S . WY) : b1 in T1 } is set
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)
{ b1 where b1 is Element of L : not Wy . b1 = Bottom (S . b1) } is set
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 | b1)) where b1 is finite Element of bool L : verum } is set
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
{ b1 where b1 is Element of bool the carrier of L : ( b1 is upper & b1 is inaccessible_by_directed_joins ) } is set
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