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 void RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict non void with_suprema with_infima complete 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 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
TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) is strict TopRelStr
the carrier of L is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
ContMaps (L,(Omega S)) is non empty V185() strict reflexive transitive antisymmetric lower-bounded non void RelStr
L is non empty TopSpace-like TopStruct
S is non empty TopSpace-like TopStruct
[:L,S:] is non empty strict TopSpace-like TopStruct
the topology of [:L,S:] is non empty Element of bool (bool the carrier of [:L,S:])
the carrier of [:L,S:] is non empty set
bool the carrier of [:L,S:] is non empty set
bool (bool the carrier of [:L,S:]) is non empty set
InclPoset the topology of [:L,S:] is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the carrier of (InclPoset the topology of [:L,S:]) is non empty non trivial set
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
InclPoset the topology of S is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of S)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of S
ContMaps (L,((InclPoset the topology of S))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (L,((InclPoset the topology of S)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (ContMaps (L,((InclPoset the topology of S)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (ContMaps (L,((InclPoset the topology of S)))):] is non empty set
the carrier of L is non empty set
Omega ((InclPoset the topology of S)) is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict non void with_suprema with_infima complete TopRelStr
oContMaps (L,((InclPoset the topology of S))) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (oContMaps (L,((InclPoset the topology of S)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (oContMaps (L,((InclPoset the topology of S)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (oContMaps (L,((InclPoset the topology of S)))):] is non empty set
S is Relation-like the carrier of (InclPoset the topology of [:L,S:]) -defined the carrier of (oContMaps (L,((InclPoset the topology of S)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:L,S:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (oContMaps (L,((InclPoset the topology of S)))):]
S is Relation-like the carrier of (InclPoset the topology of [:L,S:]) -defined the carrier of (ContMaps (L,((InclPoset the topology of S)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:L,S:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (ContMaps (L,((InclPoset the topology of S)))):]
SS is Relation-like the carrier of (InclPoset the topology of [:L,S:]) -defined the carrier of (ContMaps (L,((InclPoset the topology of S)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:L,S:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:L,S:]), the carrier of (ContMaps (L,((InclPoset the topology of S)))):]
Wy is Element of the carrier of (InclPoset the topology of [:L,S:])
S . Wy is Relation-like Function-like Element of the carrier of (ContMaps (L,((InclPoset the topology of S))))
T is Relation-like open Element of bool the carrier of [:L,S:]
(T, the carrier of L) *graph is Relation-like Function-like set
SS . Wy is Relation-like Function-like Element of the carrier of (ContMaps (L,((InclPoset the topology of S))))
{ [b1,b2] where b1 is open Element of bool the carrier of a1, b2 is Element of the carrier of a1 : b2 in b1 } is set
L is non empty TopSpace-like T_0 TopStruct
S is non empty TopSpace-like TopStruct
[:S,L:] is non empty strict TopSpace-like TopStruct
S 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 TopRelStr
ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
ContMaps ([:S,L:],S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps ([:S,L:],S)) is functional non empty set
SS is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete Scott non void TopAugmentation of ContMaps (L,S)
ContMaps (S,SS) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (S,SS)) is functional non empty set
[: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
[: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
Wy is Relation-like the carrier of (ContMaps (S,SS)) -defined the carrier of (ContMaps ([:S,L:],S)) -valued Function-like non empty V24( the carrier of (ContMaps (S,SS))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):]
T is Relation-like the carrier of (ContMaps ([:S,L:],S)) -defined the carrier of (ContMaps (S,SS)) -valued Function-like non empty V24( the carrier of (ContMaps ([:S,L:],S))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):]
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 non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr
the carrier of (ContMaps (L,S)) is functional non empty set
the InternalRel of (ContMaps (L,S)) is Relation-like the carrier of (ContMaps (L,S)) -defined the carrier of (ContMaps (L,S)) -valued non empty Element of bool [: the carrier of (ContMaps (L,S)), the carrier of (ContMaps (L,S)):]
[: the carrier of (ContMaps (L,S)), the carrier of (ContMaps (L,S)):] is non empty set
bool [: the carrier of (ContMaps (L,S)), the carrier of (ContMaps (L,S)):] is non empty set
RelStr(# the carrier of (ContMaps (L,S)), the InternalRel of (ContMaps (L,S)) #) is strict RelStr
the carrier of L is non empty set
S |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the InternalRel of (S |^ the carrier of L) is Relation-like the carrier of (S |^ the carrier of L) -defined the carrier of (S |^ the carrier of L) -valued non empty Element of bool [: the carrier of (S |^ the carrier of L), the carrier of (S |^ the carrier of L):]
the carrier of (S |^ the carrier of L) is functional non empty set
[: the carrier of (S |^ the carrier of L), the carrier of (S |^ the carrier of L):] is non empty set
bool [: the carrier of (S |^ the carrier of L), the carrier of (S |^ the carrier of L):] is non empty set
the InternalRel of (S |^ the carrier of L) |_2 the carrier of (ContMaps (L,S)) is Relation-like set
the carrier of S is non empty set
SS |^ the carrier of S is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
(S |^ the carrier of L) |^ the carrier of S is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of [:S,L:] is non empty set
S |^ the carrier of [:S,L:] is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[: the carrier of S, the carrier of L:] is non empty set
S |^ [: the carrier of S, the carrier of L:] is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(ContMaps (L,S)) |^ the carrier of S is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of ((ContMaps (L,S)) |^ the carrier of S) is functional non empty set
the carrier of ((S |^ the carrier of L) |^ the carrier of S) is functional non empty set
rng Wy is functional Element of bool the carrier of (ContMaps ([:S,L:],S))
bool the carrier of (ContMaps ([:S,L:],S)) is non empty set
dom T is functional Element of bool the carrier of (ContMaps ([:S,L:],S))
the carrier of (SS |^ the carrier of S) is functional non empty set
dom Wy is functional Element of bool the carrier of (ContMaps (S,SS))
bool the carrier of (ContMaps (S,SS)) is non empty set
Funcs ( the carrier of S, the carrier of (S |^ the carrier of L)) is functional non empty FUNCTION_DOMAIN of the carrier of S, the carrier of (S |^ the carrier of L)
the carrier of S is 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
Funcs ( the carrier of S,(Funcs ( the carrier of L, the carrier of S))) is functional non empty FUNCTION_DOMAIN of the carrier of S, Funcs ( the carrier of L, the carrier of S)
T * Wy is Relation-like the carrier of (ContMaps (S,SS)) -defined the carrier of (ContMaps (S,SS)) -valued Function-like non empty V24( the carrier of (ContMaps (S,SS))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps (S,SS)):]
[: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps (S,SS)):] is non empty set
bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps (S,SS)):] is non empty set
id (dom Wy) is Relation-like dom Wy -defined dom Wy -valued Function-like one-to-one V24( dom Wy) quasi_total Function-yielding V40() Element of bool [:(dom Wy),(dom Wy):]
[:(dom Wy),(dom Wy):] is set
bool [:(dom Wy),(dom Wy):] is non empty set
Wy " is Relation-like Function-like set
rng T is functional Element of bool the carrier of (ContMaps (S,SS))
the carrier of (S |^ the carrier of [:S,L:]) is functional non empty set
Funcs ( the carrier of [:S,L:], the carrier of S) is functional non empty FUNCTION_DOMAIN of the carrier of [:S,L:], the carrier of S
Funcs ([: the carrier of S, the carrier of L:], the carrier of S) is functional non empty FUNCTION_DOMAIN of [: the carrier of S, the carrier of L:], the carrier of S
Wy * T is Relation-like the carrier of (ContMaps ([:S,L:],S)) -defined the carrier of (ContMaps ([:S,L:],S)) -valued Function-like non empty V24( the carrier of (ContMaps ([:S,L:],S))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps ([:S,L:],S)):]
[: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
id (dom T) is Relation-like dom T -defined dom T -valued Function-like one-to-one V24( dom T) quasi_total Function-yielding V40() Element of bool [:(dom T),(dom T):]
[:(dom T),(dom T):] is set
bool [:(dom T),(dom T):] is non empty set
T " is Relation-like Function-like set
S is non empty TopSpace-like TopStruct
[:S,L:] is non empty strict TopSpace-like TopStruct
S 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 TopRelStr
ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
ContMaps ([:S,L:],S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps ([:S,L:],S)) is functional non empty set
SS is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete Scott non void TopAugmentation of ContMaps (L,S)
ContMaps (S,SS) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (S,SS)) is functional non empty set
[: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
[: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
Wy is Relation-like the carrier of (ContMaps (S,SS)) -defined the carrier of (ContMaps ([:S,L:],S)) -valued Function-like non empty V24( the carrier of (ContMaps (S,SS))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):]
T is Relation-like the carrier of (ContMaps ([:S,L:],S)) -defined the carrier of (ContMaps (S,SS)) -valued Function-like non empty V24( the carrier of (ContMaps ([:S,L:],S))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):]
L is non empty TopSpace-like TopStruct
oContMaps (L,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (oContMaps (L,Sierpinski_Space)) is functional non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
[: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
the carrier of Sierpinski_Space is non empty non trivial set
[: the carrier of L, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of L, the carrier of Sierpinski_Space:] is non empty set
S is Relation-like Function-like set
proj1 S is set
proj2 S is set
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool the carrier of Sierpinski_Space is non empty set
bool (bool the carrier of Sierpinski_Space) is non empty set
SS is set
Wy is set
S . Wy is set
T is Relation-like Function-like Element of the carrier of (oContMaps (L,Sierpinski_Space))
[#] Sierpinski_Space is non empty non proper open closed dense non boundary Element of bool the carrier of Sierpinski_Space
WY is Relation-like the carrier of L -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of Sierpinski_Space:]
S is open Element of bool the carrier of Sierpinski_Space
WY " S is Element of bool the carrier of L
S is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
SS is Relation-like the carrier of L -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of Sierpinski_Space:]
S . SS is set
SS " {1} is Element of bool the carrier of L
S is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
S is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
SS is Relation-like Function-like Element of the carrier of (oContMaps (L,Sierpinski_Space))
S . SS is Element of the carrier of (InclPoset the topology of L)
Wy is Relation-like the carrier of L -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of Sierpinski_Space:]
Wy " {1} is Element of bool the carrier of L
S . SS is Element of the carrier of (InclPoset the topology of L)
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool the carrier of Sierpinski_Space is non empty set
bool (bool the carrier of Sierpinski_Space) is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
bool the carrier of S is non empty set
oContMaps (S,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (oContMaps (S,Sierpinski_Space)) is functional non empty set
the topology of S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
InclPoset the topology of S is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the carrier of (InclPoset the topology of S) is non empty non trivial set
(S) is Relation-like the carrier of (oContMaps (S,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of S) -valued Function-like non empty V24( the carrier of (oContMaps (S,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (S,Sierpinski_Space)), the carrier of (InclPoset the topology of S):]
[: the carrier of (oContMaps (S,Sierpinski_Space)), the carrier of (InclPoset the topology of S):] is non empty set
bool [: the carrier of (oContMaps (S,Sierpinski_Space)), the carrier of (InclPoset the topology of S):] is non empty set
(S) " is Relation-like the carrier of (InclPoset the topology of S) -defined the carrier of (oContMaps (S,Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (InclPoset the topology of S)) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of S), the carrier of (oContMaps (S,Sierpinski_Space)):]
[: the carrier of (InclPoset the topology of S), the carrier of (oContMaps (S,Sierpinski_Space)):] is non empty set
bool [: the carrier of (InclPoset the topology of S), the carrier of (oContMaps (S,Sierpinski_Space)):] is non empty set
S is Relation-like the carrier of (InclPoset the topology of S) -defined the carrier of (oContMaps (S,Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (InclPoset the topology of S)) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of S), the carrier of (oContMaps (S,Sierpinski_Space)):]
rng S is functional Element of bool the carrier of (oContMaps (S,Sierpinski_Space))
bool the carrier of (oContMaps (S,Sierpinski_Space)) is non empty set
[#] (oContMaps (S,Sierpinski_Space)) is functional non empty non proper lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of (oContMaps (S,Sierpinski_Space))
S " is Relation-like the carrier of (oContMaps (S,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of S) -valued Function-like non empty V24( the carrier of (oContMaps (S,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (S,Sierpinski_Space)), the carrier of (InclPoset the topology of S):]
S " is Relation-like Function-like set
[: the carrier of S, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of S, the carrier of Sierpinski_Space:] is non empty set
SS is Relation-like Function-like Element of the carrier of (oContMaps (S,Sierpinski_Space))
[#] Sierpinski_Space is non empty non proper open closed dense non boundary Element of bool the carrier of Sierpinski_Space
Wy is Relation-like the carrier of S -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of Sierpinski_Space:]
L is open Element of bool the carrier of Sierpinski_Space
Wy " L is Element of bool the carrier of S
S . (Wy " L) is Relation-like Function-like set
chi ((Wy " L), the carrier of S) is Relation-like the carrier of S -defined {{},1} -valued Function-like quasi_total Element of bool [: the carrier of S,{{},1}:]
[: the carrier of S,{{},1}:] is set
bool [: the carrier of S,{{},1}:] is non empty set
(S) . SS is Element of the carrier of (InclPoset the topology of S)
(S ") . SS is Element of the carrier of (InclPoset the topology of S)
SS is open Element of bool the carrier of S
((S) ") . SS is Relation-like Function-like set
chi (SS, the carrier of S) is Relation-like the carrier of S -defined {{},1} -valued Function-like quasi_total Element of bool [: the carrier of S,{{},1}:]
L is non empty TopSpace-like TopStruct
oContMaps (L,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
(L) is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
the carrier of (oContMaps (L,Sierpinski_Space)) is functional non empty set
the carrier of (InclPoset the topology of L) is non empty non trivial set
[: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool the carrier of Sierpinski_Space is non empty set
bool (bool the carrier of Sierpinski_Space) is non empty set
[: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):] is non empty set
S is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (oContMaps (L,Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (InclPoset the topology of L)) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):]
S " is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
S " is Relation-like Function-like set
[: the carrier of L, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of L, the carrier of Sierpinski_Space:] is non empty set
SS is Relation-like Function-like Element of the carrier of (oContMaps (L,Sierpinski_Space))
[#] Sierpinski_Space is non empty non proper open closed dense non boundary Element of bool the carrier of Sierpinski_Space
Wy is Relation-like the carrier of L -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of L) quasi_total continuous Element of bool [: the carrier of L, the carrier of Sierpinski_Space:]
S is open Element of bool the carrier of Sierpinski_Space
Wy " S is Element of bool the carrier of L
S . (Wy " S) is Relation-like Function-like set
chi ((Wy " S), the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like quasi_total Element of bool [: the carrier of L,{{},1}:]
[: the carrier of L,{{},1}:] is set
bool [: the carrier of L,{{},1}:] is non empty set
(L) . SS is Element of the carrier of (InclPoset the topology of L)
(S ") . SS is Element of the carrier of (InclPoset the topology of L)
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
oContMaps (L,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (oContMaps (L,Sierpinski_Space)) is functional non empty set
the carrier of (InclPoset the topology of L) is non empty non trivial set
(L) is Relation-like the carrier of (oContMaps (L,Sierpinski_Space)) -defined the carrier of (InclPoset the topology of L) -valued Function-like one-to-one non empty V24( the carrier of (oContMaps (L,Sierpinski_Space))) quasi_total onto bijective monotone isomorphic Element of bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):]
[: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (oContMaps (L,Sierpinski_Space)), the carrier of (InclPoset the topology of L):] is non empty set
(L) " is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (oContMaps (L,Sierpinski_Space)) -valued Function-like non empty V24( the carrier of (InclPoset the topology of L)) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):]
[: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (oContMaps (L,Sierpinski_Space)):] is non empty set
L is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
Omega L 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
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L, the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L #) is non empty strict TopSpace-like injective monotone-convergence TopStruct
the carrier of L is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like injective TopStruct
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 InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L -valued non empty Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega L #) is strict RelStr
the InternalRel of (Omega L) is Relation-like the carrier of (Omega L) -defined the carrier of (Omega L) -valued non empty Element of bool [: the carrier of (Omega L), the carrier of (Omega L):]
[: the carrier of (Omega L), the carrier of (Omega L):] is non empty set
bool [: the carrier of (Omega L), the carrier of (Omega L):] is non empty set
RelStr(# the carrier of (Omega L), the InternalRel of (Omega L) #) is strict RelStr
L is non empty TopSpace-like TopStruct
oContMaps (L,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((BoolePoset 1)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of BoolePoset 1
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of BoolePoset 1
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
sigma (BoolePoset 1) is non empty Element of bool (bool the carrier of (BoolePoset 1))
bool the carrier of (BoolePoset 1) is non empty set
bool (bool the carrier of (BoolePoset 1)) is non empty set
Scott-Convergence (BoolePoset 1) is (CONSTANTS) (SUBNETS) Convergence-Class of BoolePoset 1
ConvergenceSpace (Scott-Convergence (BoolePoset 1)) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence (BoolePoset 1))) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence (BoolePoset 1))))
the carrier of (ConvergenceSpace (Scott-Convergence (BoolePoset 1))) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence (BoolePoset 1))) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence (BoolePoset 1)))) is non empty set
the topology of ((BoolePoset 1)) is non empty Element of bool (bool the carrier of ((BoolePoset 1)))
the carrier of ((BoolePoset 1)) is non empty set
bool the carrier of ((BoolePoset 1)) is non empty set
bool (bool the carrier of ((BoolePoset 1))) 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 InternalRel of ((BoolePoset 1)) is Relation-like the carrier of ((BoolePoset 1)) -defined the carrier of ((BoolePoset 1)) -valued non empty Element of bool [: the carrier of ((BoolePoset 1)), the carrier of ((BoolePoset 1)):]
[: the carrier of ((BoolePoset 1)), the carrier of ((BoolePoset 1)):] is non empty set
bool [: the carrier of ((BoolePoset 1)), the carrier of ((BoolePoset 1)):] is non empty set
RelStr(# the carrier of ((BoolePoset 1)), the InternalRel of ((BoolePoset 1)) #) is strict RelStr
L is non empty set
S is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> S) is non empty strict TopSpace-like T_0 V185() TopStruct
S is Element of L
(L --> S) . S is non empty TopStruct
L is non empty set
S 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
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
L --> (S) is Relation-like L -defined Function-like constant non empty V24(L) V326() RelStr-yielding non-Empty reflexive-yielding TopStruct-yielding Poset-yielding set
product (L --> (S)) is non empty strict TopSpace-like T_0 V185() injective monotone-convergence TopStruct
Omega (product (L --> (S))) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopRelStr
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() RelStr-yielding non-Empty reflexive-yielding Poset-yielding set
product (L --> S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
((product (L --> S))) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of product (L --> 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 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
Omega (S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopRelStr
the carrier of (Omega (product (L --> (S)))) is non empty set
the InternalRel of (Omega (product (L --> (S)))) is Relation-like the carrier of (Omega (product (L --> (S)))) -defined the carrier of (Omega (product (L --> (S)))) -valued non empty Element of bool [: the carrier of (Omega (product (L --> (S)))), the carrier of (Omega (product (L --> (S)))):]
[: the carrier of (Omega (product (L --> (S)))), the carrier of (Omega (product (L --> (S)))):] is non empty set
bool [: the carrier of (Omega (product (L --> (S)))), the carrier of (Omega (product (L --> (S)))):] is non empty set
RelStr(# the carrier of (Omega (product (L --> (S)))), the InternalRel of (Omega (product (L --> (S)))) #) is strict RelStr
product (L --> (S)) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(S) |^ L is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
S |^ L is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
((S |^ L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S |^ L
S is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> S) is non empty strict TopSpace-like T_0 V185() injective monotone-convergence TopStruct
Omega (product (L --> S)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopRelStr
((Omega (product (L --> S)))) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega (product (L --> S))
L is non empty set
S is non empty TopSpace-like T_0 injective monotone-convergence TopStruct
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> S) is non empty strict TopSpace-like T_0 V185() injective monotone-convergence TopStruct
Omega (product (L --> S)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopRelStr
Omega S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopRelStr
L --> (Omega S) is Relation-like L -defined Function-like constant non empty V24(L) V326() RelStr-yielding non-Empty reflexive-yielding TopStruct-yielding Poset-yielding set
product (L --> (Omega S)) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
((product (L --> (Omega S)))) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of product (L --> (Omega S))
the carrier of (Omega (product (L --> S))) is non empty set
the InternalRel of (Omega (product (L --> S))) is Relation-like the carrier of (Omega (product (L --> S))) -defined the carrier of (Omega (product (L --> S))) -valued non empty Element of bool [: the carrier of (Omega (product (L --> S))), the carrier of (Omega (product (L --> S))):]
[: the carrier of (Omega (product (L --> S))), the carrier of (Omega (product (L --> S))):] is non empty set
bool [: the carrier of (Omega (product (L --> S))), the carrier of (Omega (product (L --> S))):] is non empty set
RelStr(# the carrier of (Omega (product (L --> S))), the InternalRel of (Omega (product (L --> S))) #) is strict RelStr
((Omega (product (L --> S)))) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott satisfying_axiom_of_approximation continuous injective non void monotone-convergence with_suprema with_infima complete TopAugmentation of Omega (product (L --> S))
S is non empty TopSpace-like TopStruct
L is non empty set
S is non empty TopSpace-like TopStruct
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> S) is non empty strict TopSpace-like V185() TopStruct
oContMaps (S,(product (L --> S))) is non empty V185() strict reflexive transitive non void RelStr
the carrier of (oContMaps (S,(product (L --> S)))) is functional non empty set
oContMaps (S,S) is non empty V185() strict reflexive transitive non void RelStr
(oContMaps (S,S)) |^ L is non empty V185() strict reflexive transitive non void RelStr
the carrier of ((oContMaps (S,S)) |^ L) is functional non empty set
[: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):] is non empty set
bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):] is non empty set
the carrier of S is non empty set
the carrier of (product (L --> S)) is functional non empty set
[: the carrier of S, the carrier of (product (L --> S)):] is non empty set
bool [: the carrier of S, the carrier of (product (L --> S)):] is non empty set
SS is Relation-like the carrier of (oContMaps (S,(product (L --> S)))) -defined the carrier of ((oContMaps (S,S)) |^ L) -valued Function-like non empty V24( the carrier of (oContMaps (S,(product (L --> S))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):]
Wy is Relation-like the carrier of (oContMaps (S,(product (L --> S)))) -defined the carrier of ((oContMaps (S,S)) |^ L) -valued Function-like non empty V24( the carrier of (oContMaps (S,(product (L --> S))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):]
T is Relation-like Function-like Element of the carrier of (oContMaps (S,(product (L --> S))))
SS . T is Relation-like Function-like Element of the carrier of ((oContMaps (S,S)) |^ L)
WY is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
commute WY is Relation-like Function-like Function-yielding V40() set
Wy . T is Relation-like Function-like Element of the carrier of ((oContMaps (S,S)) |^ L)
SS is Relation-like Function-like set
proj1 SS is set
proj2 SS is set
Wy is set
T is set
SS . T is set
WY is Relation-like Function-like Element of the carrier of (oContMaps (S,(product (L --> S))))
T1 is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
commute T1 is Relation-like Function-like Function-yielding V40() set
the carrier of (oContMaps (S,S)) is functional non empty set
[:L, the carrier of (oContMaps (S,S)):] is non empty set
bool [:L, the carrier of (oContMaps (S,S)):] is non empty set
commute WY is Relation-like Function-like Function-yielding V40() set
Funcs (L, the carrier of (oContMaps (S,S))) is functional non empty FUNCTION_DOMAIN of L, the carrier of (oContMaps (S,S))
Wy is Relation-like the carrier of (oContMaps (S,(product (L --> S)))) -defined the carrier of ((oContMaps (S,S)) |^ L) -valued Function-like non empty V24( the carrier of (oContMaps (S,(product (L --> S))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):]
T is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
Wy . T is Relation-like Function-like set
commute T is Relation-like Function-like Function-yielding V40() set
L is non empty set
S is non empty TopSpace-like TopStruct
S is non empty TopSpace-like TopStruct
(L,S,S) is Relation-like the carrier of (oContMaps (S,(product (L --> S)))) -defined the carrier of ((oContMaps (S,S)) |^ L) -valued Function-like non empty V24( the carrier of (oContMaps (S,(product (L --> S))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):]
L --> S is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> S) is non empty strict TopSpace-like V185() TopStruct
oContMaps (S,(product (L --> S))) is non empty V185() strict reflexive transitive non void RelStr
the carrier of (oContMaps (S,(product (L --> S)))) is functional non empty set
oContMaps (S,S) is non empty V185() strict reflexive transitive non void RelStr
(oContMaps (S,S)) |^ L is non empty V185() strict reflexive transitive non void RelStr
the carrier of ((oContMaps (S,S)) |^ L) is functional non empty set
[: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):] is non empty set
bool [: the carrier of (oContMaps (S,(product (L --> S)))), the carrier of ((oContMaps (S,S)) |^ L):] is non empty set
Carrier (L --> S) is Relation-like L -defined Function-like V24(L) set
the carrier of S is non empty set
L --> the carrier of S is Relation-like non-empty L -defined Function-like constant non empty V24(L) set
the carrier of (product (L --> S)) is functional non empty set
product (L --> the carrier of S) is set
Funcs (L, the carrier of S) is functional non empty FUNCTION_DOMAIN of L, the carrier of S
the carrier of S is non empty set
Funcs ( the carrier of S,(Funcs (L, the carrier of S))) is functional non empty FUNCTION_DOMAIN of the carrier of S, Funcs (L, the carrier of S)
Wy is set
T is set
[: the carrier of S, the carrier of (product (L --> S)):] is non empty set
bool [: the carrier of S, the carrier of (product (L --> S)):] is non empty set
WY is Relation-like Function-like Element of the carrier of (oContMaps (S,(product (L --> S))))
T1 is Relation-like Function-like Element of the carrier of (oContMaps (S,(product (L --> S))))
(L,S,S) . Wy is Relation-like Function-like set
(L,S,S) . T is Relation-like Function-like set
wy is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
commute wy is Relation-like Function-like Function-yielding V40() set
x is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
commute x is Relation-like Function-like Function-yielding V40() set
commute (commute x) is Relation-like Function-like Function-yielding V40() set
rng (L,S,S) is functional Element of bool the carrier of ((oContMaps (S,S)) |^ L)
bool the carrier of ((oContMaps (S,S)) |^ L) is non empty set
Wy is set
the carrier of (oContMaps (S,S)) is functional non empty set
Funcs (L, the carrier of (oContMaps (S,S))) is functional non empty FUNCTION_DOMAIN of L, the carrier of (oContMaps (S,S))
[:L, the carrier of (oContMaps (S,S)):] is non empty set
bool [:L, the carrier of (oContMaps (S,S)):] is non empty set
T is Relation-like Function-like Element of the carrier of ((oContMaps (S,S)) |^ L)
WY is Relation-like L -defined the carrier of (oContMaps (S,S)) -valued Function-like non empty V24(L) quasi_total Function-yielding V40() Element of bool [:L, the carrier of (oContMaps (S,S)):]
commute WY is Relation-like Function-like Function-yielding V40() set
T1 is Relation-like the carrier of S -defined the carrier of (product (L --> S)) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() continuous Element of bool [: the carrier of S, the carrier of (product (L --> S)):]
Funcs ( the carrier of S, the carrier of S) is functional non empty FUNCTION_DOMAIN of the carrier of S, the carrier of S
Funcs (L,(Funcs ( the carrier of S, the carrier of S))) is functional non empty FUNCTION_DOMAIN of L, Funcs ( the carrier of S, the carrier of S)
commute (commute WY) is Relation-like Function-like Function-yielding V40() set
wy is Relation-like Function-like Element of the carrier of (oContMaps (S,(product (L --> S))))
(L,S,S) . wy is Relation-like Function-like Element of the carrier of ((oContMaps (S,S)) |^ L)
dom (L,S,S) is functional Element of bool the carrier of (oContMaps (S,(product (L --> S))))
bool the carrier of (oContMaps (S,(product (L --> S)))) is non empty set
S is non empty TopSpace-like TopStruct
L is non empty set
L --> Sierpinski_Space is Relation-like L -defined Function-like constant non empty V24(L) V326() non-Empty TopStruct-yielding set
product (L --> Sierpinski_Space) is non empty strict TopSpace-like T_0 V185() injective monotone-convergence TopStruct
oContMaps (S,(product (L --> Sierpinski_Space))) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
oContMaps (S,Sierpinski_Space) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(oContMaps (S,Sierpinski_Space)) |^ L is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(L,S,Sierpinski_Space) is Relation-like the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))) -defined the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L) -valued Function-like one-to-one non empty V24( the carrier of (oContMaps (S,(product (L --> Sierpinski_Space))))) quasi_total onto bijective Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))), the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L):]
the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))) is functional non empty set
the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L) is functional non empty set
[: the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))), the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L):] is non empty set
bool [: the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))), the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L):] is non empty set
L --> (oContMaps (S,Sierpinski_Space)) is Relation-like L -defined Function-like constant non empty V24(L) V326() RelStr-yielding non-Empty reflexive-yielding Poset-yielding set
product (L --> (oContMaps (S,Sierpinski_Space))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of S is non empty set
the carrier of (product (L --> Sierpinski_Space)) is functional non empty set
[: the carrier of S, the carrier of (product (L --> Sierpinski_Space)):] is non empty set
bool [: the carrier of S, the carrier of (product (L --> Sierpinski_Space)):] is non empty set
S is Relation-like the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))) -defined the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L) -valued Function-like non empty V24( the carrier of (oContMaps (S,(product (L --> Sierpinski_Space))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (oContMaps (S,(product (L --> Sierpinski_Space)))), the carrier of ((oContMaps (S,Sierpinski_Space)) |^ L):]
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of SS is non empty set
[: the carrier of S, the carrier of SS:] is non empty set
bool [: the carrier of S, the carrier of SS:] is non empty 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
sigma (InclPoset the topology of L) is non empty Element of bool (bool the carrier of (InclPoset the topology of L))
the carrier of (InclPoset the topology of L) is non empty non trivial set
bool the carrier of (InclPoset the topology of L) is non empty set
bool (bool the carrier of (InclPoset the topology of L)) is non empty set
Scott-Convergence (InclPoset the topology of L) is (CONSTANTS) (SUBNETS) Convergence-Class of InclPoset the topology of L
ConvergenceSpace (Scott-Convergence (InclPoset the topology of L)) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence (InclPoset the topology of L))) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence (InclPoset the topology of L))))
the carrier of (ConvergenceSpace (Scott-Convergence (InclPoset the topology of L))) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence (InclPoset the topology of L))) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence (InclPoset the topology of L)))) is non empty set
Wy is Relation-like the carrier of S -defined the carrier of SS -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of SS:]
*graph Wy is Relation-like set
the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) is strict RelStr
the carrier of ((InclPoset the topology of L)) is non empty set
the InternalRel of ((InclPoset the topology of L)) is Relation-like the carrier of ((InclPoset the topology of L)) -defined the carrier of ((InclPoset the topology of L)) -valued non empty Element of bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):]
[: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
RelStr(# the carrier of ((InclPoset the topology of L)), the InternalRel of ((InclPoset the topology of L)) #) is strict RelStr
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 non empty strict TopSpace-like TopStruct
TopRelStr(# the carrier of SS, the InternalRel of SS, the topology of SS #) is strict TopRelStr
the topology of ((InclPoset the topology of L)) is non empty Element of bool (bool the carrier of ((InclPoset the topology of L)))
bool the carrier of ((InclPoset the topology of L)) is non empty set
bool (bool the carrier of ((InclPoset the topology of L))) is non empty set
TopRelStr(# the carrier of ((InclPoset the topology of L)), the InternalRel of ((InclPoset the topology of L)), the topology of ((InclPoset the topology of L)) #) is strict TopRelStr
the topology of [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
bool (bool the carrier of [:S,L:]) is non empty set
InclPoset the topology of [:S,L:] is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the carrier of (InclPoset the topology of [:S,L:]) is non empty non trivial set
ContMaps (S,SS) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (S,SS)) is functional non empty set
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,SS)):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,SS)):] is non empty set
(S,L) is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
ContMaps (S,((InclPoset the topology of L))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (S,((InclPoset the topology of L)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
T is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (ContMaps (S,SS)) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,SS)):]
rng T is functional Element of bool the carrier of (ContMaps (S,SS))
bool the carrier of (ContMaps (S,SS)) is non empty set
dom T is Element of bool the carrier of (InclPoset the topology of [:S,L:])
bool the carrier of (InclPoset the topology of [:S,L:]) is non empty set
WY is set
T . WY is Relation-like Function-like set
[: the carrier of S, the carrier of L:] is non empty set
bool [: the carrier of S, the carrier of L:] is non empty set
T1 is Relation-like open Element of bool the carrier of [:S,L:]
wy is Relation-like the carrier of S -defined the carrier of L -valued Element of bool [: the carrier of S, the carrier of L:]
dom wy is Element of bool the carrier of S
(T1, the carrier of S) *graph is Relation-like Function-like set
S is non empty TopSpace-like TopStruct
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
InclPoset the topology of S is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive 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 monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of S
ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (L,S)) is functional non empty set
SS is Relation-like Function-like Element of the carrier of (ContMaps (L,S))
Wy is Relation-like Function-like Element of the carrier of (ContMaps (L,S))
*graph SS is Relation-like set
*graph Wy is Relation-like set
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
T1 is set
wy is set
[T1,wy] is non empty set
{T1,wy} is finite set
{T1} is trivial finite set
{{T1,wy},{T1}} is finite V45() 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 (InclPoset the topology of S) is non empty non trivial set
the InternalRel of (InclPoset the topology of S) is Relation-like the carrier of (InclPoset the topology of S) -defined the carrier of (InclPoset the topology of S) -valued non empty Element of bool [: the carrier of (InclPoset the topology of S), the carrier of (InclPoset the topology of S):]
[: the carrier of (InclPoset the topology of S), the carrier of (InclPoset the topology of S):] is non empty set
bool [: the carrier of (InclPoset the topology of S), the carrier of (InclPoset the topology of S):] is non empty set
RelStr(# the carrier of (InclPoset the topology of S), the InternalRel of (InclPoset the topology of S) #) is strict RelStr
proj1 Wy is set
proj1 SS is set
SS . T1 is set
T 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:]
x is Element of the carrier of L
T . x is Element of the carrier of S
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 . x is Element of the carrier of S
Wy . T1 is set
SS . x is set
Wy . x is set
[(SS . x),(Wy . x)] is non empty set
{(SS . x),(Wy . x)} is finite set
{(SS . x)} is trivial finite set
{{(SS . x),(Wy . x)},{(SS . x)}} is finite V45() set
[(SS . T1),(Wy . T1)] is non empty set
{(SS . T1),(Wy . T1)} is finite set
{(SS . T1)} is trivial finite set
{{(SS . T1),(Wy . T1)},{(SS . T1)}} is finite V45() set
RelIncl the topology of S is Relation-like the topology of S -defined the topology of S -valued V16() V19() V23() V24( the topology of S) quasi_total Element of bool [: the topology of S, the topology of S:]
[: the topology of S, the topology of S:] is non empty set
bool [: the topology of S, the topology of S:] is non empty set
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
S is non empty TopSpace-like TopStruct
[:S,L:] is non empty strict TopSpace-like TopStruct
the topology of [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
InclPoset the topology of [:S,L:] is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
ContMaps (S,((InclPoset the topology of L))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
(S,L) is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
the carrier of (InclPoset the topology of [:S,L:]) is non empty non trivial set
the carrier of (ContMaps (S,((InclPoset the topology of L)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
SS is Relation-like Function-like set
proj1 SS is set
proj2 SS is set
Wy is set
T is set
SS . T is set
the carrier of S is non empty set
the carrier of ((InclPoset the topology of L)) is non empty set
[: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
WY is Relation-like Function-like Element of the carrier of (ContMaps (S,((InclPoset the topology of L))))
T1 is Relation-like the carrier of S -defined the carrier of ((InclPoset the topology of L)) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):]
*graph T1 is Relation-like set
[: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (InclPoset the topology of [:S,L:]):] is non empty set
bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (InclPoset the topology of [:S,L:]):] is non empty set
oContMaps (S,((InclPoset the topology of L))) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (oContMaps (S,((InclPoset the topology of L)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (oContMaps (S,((InclPoset the topology of L)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (oContMaps (S,((InclPoset the topology of L)))):] is non empty set
the carrier of S is non empty set
T is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (oContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (oContMaps (S,((InclPoset the topology of L)))):]
Wy is Relation-like the carrier of (ContMaps (S,((InclPoset the topology of L)))) -defined the carrier of (InclPoset the topology of [:S,L:]) -valued Function-like non empty V24( the carrier of (ContMaps (S,((InclPoset the topology of L))))) quasi_total Element of bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (InclPoset the topology of [:S,L:]):]
WY is Relation-like Function-like Element of the carrier of (ContMaps (S,((InclPoset the topology of L))))
T1 is Relation-like Function-like Element of the carrier of (ContMaps (S,((InclPoset the topology of L))))
Wy . WY is Element of the carrier of (InclPoset the topology of [:S,L:])
Wy . T1 is Element of the carrier of (InclPoset the topology of [:S,L:])
*graph WY is Relation-like set
*graph T1 is Relation-like set
Wy . WY is Element of the carrier of (InclPoset the topology of [:S,L:])
Wy . T1 is Element of the carrier of (InclPoset the topology of [:S,L:])
WY is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
dom WY is Element of bool the carrier of (InclPoset the topology of [:S,L:])
bool the carrier of (InclPoset the topology of [:S,L:]) is non empty set
rng Wy is Element of bool the carrier of (InclPoset the topology of [:S,L:])
WY * Wy is Relation-like the carrier of (ContMaps (S,((InclPoset the topology of L)))) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (ContMaps (S,((InclPoset the topology of L))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
[: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
dom (WY * Wy) is functional Element of bool the carrier of (ContMaps (S,((InclPoset the topology of L))))
bool the carrier of (ContMaps (S,((InclPoset the topology of L)))) is non empty set
T1 is set
the carrier of ((InclPoset the topology of L)) is non empty set
[: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
wy is Relation-like the carrier of S -defined the carrier of ((InclPoset the topology of L)) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):]
*graph wy is Relation-like set
dom wy is Element of bool the carrier of S
bool the carrier of S is non empty set
y is set
{y} is trivial finite set
wy . y is set
x is Relation-like open Element of bool the carrier of [:S,L:]
Im (x,y) is set
x .: {y} is set
x1 is set
[y,x1] is non empty set
{y,x1} is finite set
{{y,x1},{y}} is finite V45() set
x1 is set
[y,x1] is non empty set
{y,x1} is finite set
{{y,x1},{y}} is finite V45() set
x2 is set
[x2,x1] is non empty set
{x2,x1} is finite set
{x2} is trivial finite set
{{x2,x1},{x2}} is finite V45() set
(WY * Wy) . T1 is Relation-like Function-like set
Wy . wy is set
WY . (Wy . wy) is Relation-like Function-like set
WY . x is Relation-like Function-like set
(x, the carrier of S) *graph is Relation-like Function-like set
id (ContMaps (S,((InclPoset the topology of L)))) is Relation-like the carrier of (ContMaps (S,((InclPoset the topology of L)))) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like one-to-one non empty V24( the carrier of (ContMaps (S,((InclPoset the topology of L))))) quasi_total onto bijective Function-yielding V40() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376( ContMaps (S,((InclPoset the topology of L)))) V377( ContMaps (S,((InclPoset the topology of L)))) V378( ContMaps (S,((InclPoset the topology of L)))) Element of bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
id the carrier of (ContMaps (S,((InclPoset the topology of L)))) is Relation-like the carrier of (ContMaps (S,((InclPoset the topology of L)))) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like one-to-one non empty V24( the carrier of (ContMaps (S,((InclPoset the topology of L))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (ContMaps (S,((InclPoset the topology of L)))), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
Wy * WY is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (InclPoset the topology of [:S,L:]) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (InclPoset the topology of [:S,L:]):]
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (InclPoset the topology of [:S,L:]):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (InclPoset the topology of [:S,L:]):] is non empty set
dom (Wy * WY) is Element of bool the carrier of (InclPoset the topology of [:S,L:])
T1 is set
wy is Relation-like open Element of bool the carrier of [:S,L:]
(wy, the carrier of S) *graph is Relation-like Function-like set
[: the carrier of S, the carrier of L:] is non empty set
proj1 wy is set
y is set
x1 is set
[y,x1] is non empty set
{y,x1} is finite set
{y} is trivial finite set
{{y,x1},{y}} is finite V45() set
(Wy * WY) . T1 is set
WY . wy is Relation-like Function-like set
Wy . (WY . wy) is set
x is Relation-like Function-like Element of the carrier of (ContMaps (S,((InclPoset the topology of L))))
Wy . x is Element of the carrier of (InclPoset the topology of [:S,L:])
*graph x is Relation-like set
id (InclPoset the topology of [:S,L:]) is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (InclPoset the topology of [:S,L:]) -valued Function-like one-to-one non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total onto bijective monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376( InclPoset the topology of [:S,L:]) V377( InclPoset the topology of [:S,L:]) V378( InclPoset the topology of [:S,L:]) Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (InclPoset the topology of [:S,L:]):]
id the carrier of (InclPoset the topology of [:S,L:]) is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (InclPoset the topology of [:S,L:]) -valued Function-like one-to-one non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (InclPoset the topology of [:S,L:]):]
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
{ [b1,b2] where b1 is open Element of bool the carrier of L, b2 is Element of the carrier of L : b2 in b1 } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
[:S,L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
the carrier of S is non empty set
[: 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
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total onto bijective continuous open monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(S) V377(S) V378(S) Element of bool [: the carrier of S, the carrier of S:]
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
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:]
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
the InternalRel of (InclPoset the topology of L) is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (InclPoset the topology of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):]
[: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of L), the InternalRel of (InclPoset the topology of L) #) is strict RelStr
S is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph S is Relation-like set
SS is set
Wy is set
[SS,Wy] is non empty set
{SS,Wy} is finite set
{SS} is trivial finite set
{{SS,Wy},{SS}} is finite V45() set
dom S is Element of bool the carrier of S
bool the carrier of S is non empty set
S . SS is set
T is open Element of bool the carrier of L
S . T is set
WY is Element of the carrier of L
SS is set
Wy is open Element of bool the carrier of L
T is Element of the carrier of L
[Wy,T] is non empty set
{Wy,T} is finite set
{Wy} is trivial finite set
{{Wy,T},{Wy}} is finite V45() set
dom S is Element of bool the carrier of S
bool the carrier of S is non empty set
S . Wy is set
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
{ [b1,b2] where b1 is open Element of bool the carrier of L, b2 is Element of the carrier of L : b2 in b1 } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
[:S,L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
SS is Element of the carrier of L
Wy is non empty open a_neighborhood of SS
the topology of S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of S, b2 is Element of bool the carrier of L : ( b1 in the topology of S & b2 in the topology of L ) } is set
[Wy,SS] is non empty set
{Wy,SS} is finite set
{Wy} is trivial finite set
{{Wy,SS},{Wy}} is finite V45() set
S is Relation-like open Element of bool the carrier of [:S,L:]
T is open V99([:S,L:]) Element of bool (bool the carrier of [:S,L:])
WY is Relation-like Element of bool the carrier of [:S,L:]
T1 is Element of bool the carrier of S
wy is Element of bool the carrier of L
[:T1,wy:] is Relation-like Element of bool the carrier of [:S,L:]
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 (InclPoset the topology of L) is non empty non trivial set
the InternalRel of (InclPoset the topology of L) is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (InclPoset the topology of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):]
[: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of L), the InternalRel of (InclPoset the topology of L) #) is strict RelStr
x is open upper inaccessible_by_directed_joins Element of bool the carrier of S
meet x is set
y is set
x1 is set
x1 is open Element of bool the carrier of L
y is Element of bool the carrier of L
x2 is set
u2 is set
[u2,x2] is non empty set
{u2,x2} is finite set
{u2} is trivial finite set
{{u2,x2},{u2}} is finite V45() set
u1 is open Element of bool the carrier of L
y1 is Element of the carrier of L
[u1,y1] is non empty set
{u1,y1} is finite set
{u1} is trivial finite set
{{u1,y1},{u1}} is finite V45() set
Int y is open Element of bool the carrier of L
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
[: 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
SS is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph SS is Relation-like 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
bool (bool the carrier of [:S,L:]) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of S, b2 is Element of bool the carrier of L : ( b1 in the topology of S & b2 in the topology of L ) } is 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 (InclPoset the topology of L) is non empty non trivial set
the InternalRel of (InclPoset the topology of L) is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (InclPoset the topology of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):]
[: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of L), the InternalRel of (InclPoset the topology of L) #) is strict RelStr
T is set
WY is set
T1 is set
[WY,T1] is non empty set
{WY,T1} is finite set
{WY} is trivial finite set
{{WY,T1},{WY}} is finite V45() set
dom SS is Element of bool the carrier of S
SS . WY is set
rng SS is Element of bool the carrier of S
bool the carrier of S is non empty set
[: the carrier of S, the carrier of L:] is non empty set
WY is Element of the carrier of [:S,L:]
T is Relation-like Element of bool the carrier of [:S,L:]
T1 is set
wy is set
[T1,wy] is non empty set
{T1,wy} is finite set
{T1} is trivial finite set
{{T1,wy},{T1}} is finite V45() set
SS . T1 is set
x is Element of the carrier of S
SS . x is Element of the carrier of S
y is Element of the carrier of L
x1 is open Element of bool the carrier of L
Int x1 is open Element of bool the carrier of L
x2 is non empty open a_neighborhood of y
u2 is open upper inaccessible_by_directed_joins Element of bool the carrier of S
meet u2 is set
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of S
SS " u2 is Element of bool the carrier of S
y1 is non empty a_neighborhood of y
Int y1 is open Element of bool the carrier of L
Int (Int y1) is open Element of bool the carrier of L
u1 is open Element of bool the carrier of S
y2 is non empty open a_neighborhood of y
[:u1,y2:] is Relation-like Element of bool the carrier of [:S,L:]
y1 is Relation-like Element of bool the carrier of [:S,L:]
y2 is Relation-like Element of bool the carrier of [:S,L:]
Wy is open V99([:S,L:]) Element of bool (bool the carrier of [:S,L:])
v2 is set
v1 is set
[v2,v1] is non empty set
{v2,v1} is finite set
{v2} is trivial finite set
{{v2,v1},{v2}} is finite V45() set
SS . v2 is set
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of (InclPoset the topology of L) is non empty non trivial set
SS is Element of the carrier of (InclPoset the topology of L)
waybelow SS is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below SS } is set
Wy is Element of the carrier of (InclPoset the topology of L)
waybelow Wy is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below Wy } is set
SS is Element of the carrier of (InclPoset the topology of L)
waybelow SS is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below SS } is set
"\/" ((waybelow SS),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L -valued non empty Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L #) is strict RelStr
the InternalRel of (InclPoset the topology of L) is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (InclPoset the topology of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):]
[: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of L), the InternalRel of (InclPoset the topology of L) #) is strict RelStr
T is set
Wy is open Element of bool the carrier of L
WY is Element of the carrier of L
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L is non empty set
T1 is non empty open a_neighborhood of WY
wy is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
meet wy is set
x is non empty a_neighborhood of WY
Int x is open Element of bool the carrier of L
x1 is Element of the carrier of (InclPoset the topology of L)
x2 is non empty directed Element of bool the carrier of (InclPoset the topology of L)
"\/" (x2,(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
y is Element of bool the carrier of (InclPoset the topology of L)
u2 is set
u1 is Element of the carrier of (InclPoset the topology of L)
union (waybelow SS) is set
union (waybelow SS) is set
downarrow SS is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
K196( the carrier of (InclPoset the topology of L),SS) is trivial finite Element of bool the carrier of (InclPoset the topology of L)
downarrow K196( the carrier of (InclPoset the topology of L),SS) is lower Element of bool the carrier of (InclPoset the topology of L)
union (downarrow SS) is set
"\/" ((downarrow SS),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
S is Element of the carrier of L
SS is non empty open a_neighborhood of S
Int SS is open Element of bool the carrier of L
the carrier of (InclPoset the topology of L) is non empty non trivial set
Wy is Element of the carrier of (InclPoset the topology of L)
waybelow Wy is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below Wy } is set
"\/" ((waybelow Wy),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
union (waybelow Wy) is set
T is set
the InternalRel of (InclPoset the topology of L) is Relation-like the carrier of (InclPoset the topology of L) -defined the carrier of (InclPoset the topology of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):]
[: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
bool [: the carrier of (InclPoset the topology of L), the carrier of (InclPoset the topology of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of L), the InternalRel of (InclPoset the topology 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
WY is Element of the carrier of (InclPoset the topology of L)
uparrow WY is non empty filtered upper Element of bool the carrier of (InclPoset the topology of L)
K196( the carrier of (InclPoset the topology of L),WY) is trivial finite Element of bool the carrier of (InclPoset the topology of L)
uparrow K196( the carrier of (InclPoset the topology of L),WY) is upper Element of bool the carrier of (InclPoset the topology of L)
meet (uparrow WY) is set
x is set
y is set
x1 is Element of the carrier of (InclPoset the topology of L)
T1 is Element of the carrier of S
wayabove T1 is upper Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : T1 is_way_below b1 } is set
x is open upper inaccessible_by_directed_joins Element of bool the carrier of S
meet x is set
wayabove WY is upper Element of bool the carrier of (InclPoset the topology of L)
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : WY is_way_below b1 } is set
y is set
meet (wayabove WY) is set
meet (wayabove T1) is set
wy is open Element of bool the carrier of L
y is Element of bool the carrier of L
Int y is open Element of bool the carrier of L
L is non empty TopSpace-like T_0 TopStruct
S 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 TopRelStr
ContMaps (L,S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
Wy is non empty TopSpace-like T_0 TopStruct
WY 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 TopRelStr
ContMaps (Wy,WY) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
S is non empty TopSpace-like TopStruct
SS is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete Scott non void TopAugmentation of ContMaps (L,S)
ContMaps (S,SS) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (S,SS)) is functional non empty set
[:S,L:] is non empty strict TopSpace-like TopStruct
ContMaps ([:S,L:],S) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps ([:S,L:],S)) is functional non empty set
[: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
bool [: the carrier of (ContMaps (S,SS)), the carrier of (ContMaps ([:S,L:],S)):] is non empty set
[: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
bool [: the carrier of (ContMaps ([:S,L:],S)), the carrier of (ContMaps (S,SS)):] is non empty set
T is non empty TopSpace-like TopStruct
T1 is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete Scott non void TopAugmentation of ContMaps (Wy,WY)
ContMaps (T,T1) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps (T,T1)) is functional non empty set
[:T,Wy:] is non empty strict TopSpace-like TopStruct
ContMaps ([:T,Wy:],WY) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of (ContMaps ([:T,Wy:],WY)) is functional non empty set
[: the carrier of (ContMaps (T,T1)), the carrier of (ContMaps ([:T,Wy:],WY)):] is non empty set
bool [: the carrier of (ContMaps (T,T1)), the carrier of (ContMaps ([:T,Wy:],WY)):] is non empty set
[: the carrier of (ContMaps ([:T,Wy:],WY)), the carrier of (ContMaps (T,T1)):] is non empty set
bool [: the carrier of (ContMaps ([:T,Wy:],WY)), the carrier of (ContMaps (T,T1)):] is non empty set
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
[: 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
SS is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph SS is Relation-like set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is non empty TopSpace-like TopStruct
[:S,L:] is non empty strict TopSpace-like TopStruct
the topology of [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
InclPoset the topology of [:S,L:] is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
ContMaps (S,((InclPoset the topology of L))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
(S,L) is Relation-like the carrier of (InclPoset the topology of [:S,L:]) -defined the carrier of (ContMaps (S,((InclPoset the topology of L)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:S,L:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):]
the carrier of (InclPoset the topology of [:S,L:]) is non empty non trivial set
the carrier of (ContMaps (S,((InclPoset the topology of L)))) is functional non empty set
[: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:S,L:]), the carrier of (ContMaps (S,((InclPoset the topology of L)))):] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
[: 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
SS is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph SS is Relation-like set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
{ [b1,b2] where b1 is open Element of bool the carrier of L, b2 is Element of the carrier of L : b2 in b1 } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
[:S,L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of ((InclPoset the topology of L)) is non empty set
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
S is Relation-like the carrier of S -defined the carrier of ((InclPoset the topology of L)) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):]
*graph S is Relation-like set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
[: 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
SS is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph SS is Relation-like 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 InternalRel of ((InclPoset the topology of L)) is Relation-like the carrier of ((InclPoset the topology of L)) -defined the carrier of ((InclPoset the topology of L)) -valued non empty Element of bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):]
[: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
RelStr(# the carrier of ((InclPoset the topology of L)), the InternalRel of ((InclPoset the topology of L)) #) is strict RelStr
[: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):] is non empty 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 non empty strict TopSpace-like TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
the topology of ((InclPoset the topology of L)) is non empty Element of bool (bool the carrier of ((InclPoset the topology of L)))
bool the carrier of ((InclPoset the topology of L)) is non empty set
bool (bool the carrier of ((InclPoset the topology of L))) is non empty set
TopStruct(# the carrier of ((InclPoset the topology of L)), the topology of ((InclPoset the topology of L)) #) is non empty strict TopSpace-like monotone-convergence TopStruct
Wy is Relation-like the carrier of S -defined the carrier of ((InclPoset the topology of L)) -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of ((InclPoset the topology of L)):]
{ [b1,b2] where b1 is open Element of bool the carrier of L, b2 is Element of the carrier of L : b2 in b1 } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
[:S,L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
{ [b1,b2] where b1 is open Element of bool the carrier of L, b2 is Element of the carrier of L : b2 in b1 } is set
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
[:((InclPoset the topology of L)),L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:((InclPoset the topology of L)),L:] is non empty set
bool the carrier of [:((InclPoset the topology of L)),L:] is non empty set
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
[: 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
SS is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
*graph SS is Relation-like set
[:S,L:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
[:S,L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
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 ((InclPoset the topology of L)) is non empty set
the InternalRel of ((InclPoset the topology of L)) is Relation-like the carrier of ((InclPoset the topology of L)) -defined the carrier of ((InclPoset the topology of L)) -valued non empty Element of bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):]
[: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
RelStr(# the carrier of ((InclPoset the topology of L)), the InternalRel of ((InclPoset the topology of L)) #) is strict RelStr
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
the topology of ((InclPoset the topology of L)) is non empty Element of bool (bool the carrier of ((InclPoset the topology of L)))
bool the carrier of ((InclPoset the topology of L)) is non empty set
bool (bool the carrier of ((InclPoset the topology of L))) is non empty set
TopStruct(# the carrier of ((InclPoset the topology of L)), the topology of ((InclPoset the topology of L)) #) is non empty strict TopSpace-like monotone-convergence TopStruct
S is Element of the carrier of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
SS is non empty open a_neighborhood of S
L is non empty TopSpace-like T_0 TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of L)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of ((InclPoset the topology of L)) is non empty set
bool the carrier of ((InclPoset the topology of L)) is non empty set
S is Element of the carrier of L
S is non empty open a_neighborhood of S
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of L
the carrier of S is non empty set
bool the carrier of S is non empty set
S is Element of the carrier of L
SS is non empty open a_neighborhood of S
Wy is open upper inaccessible_by_directed_joins Element of bool the carrier of ((InclPoset the topology of L))
meet Wy is 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 InternalRel of ((InclPoset the topology of L)) is Relation-like the carrier of ((InclPoset the topology of L)) -defined the carrier of ((InclPoset the topology of L)) -valued non empty Element of bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):]
[: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
bool [: the carrier of ((InclPoset the topology of L)), the carrier of ((InclPoset the topology of L)):] is non empty set
RelStr(# the carrier of ((InclPoset the topology of L)), the InternalRel of ((InclPoset the topology of L)) #) is strict RelStr
the topology of S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
the topology of ((InclPoset the topology of L)) is non empty Element of bool (bool the carrier of ((InclPoset the topology of L)))
bool (bool the carrier of ((InclPoset the topology of L))) is non empty set
T is Element of bool the carrier of S
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:SS,S:] is non empty strict TopSpace-like T_0 TopStruct
Wy is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
the carrier of Wy is non empty set
the topology of Wy is non empty Element of bool (bool the carrier of Wy)
bool the carrier of Wy is non empty set
bool (bool the carrier of Wy) is non empty set
TopStruct(# the carrier of Wy, the topology of Wy #) is non empty strict TopSpace-like monotone-convergence TopStruct
the topology of [:SS,S:] is non empty Element of bool (bool the carrier of [:SS,S:])
the carrier of [:SS,S:] is non empty set
bool the carrier of [:SS,S:] is non empty set
bool (bool the carrier of [:SS,S:]) is non empty set
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
the InternalRel of Wy is Relation-like the carrier of Wy -defined the carrier of Wy -valued non empty 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
RelStr(# the carrier of Wy, the InternalRel of Wy #) is strict RelStr
the InternalRel of [:S,L:] is Relation-like the carrier of [:S,L:] -defined the carrier of [:S,L:] -valued non empty Element of bool [: the carrier of [:S,L:], the carrier of [:S,L:]:]
[: the carrier of [:S,L:], the carrier of [:S,L:]:] is non empty set
bool [: the carrier of [:S,L:], the carrier of [:S,L:]:] is non empty set
RelStr(# the carrier of [:S,L:], the InternalRel of [:S,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
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 SS is non empty set
the InternalRel of SS is Relation-like the carrier of SS -defined the carrier of SS -valued non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) 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
[: the carrier of SS, the carrier of S:] is non empty set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:SS,S:] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:SS,S:] is non empty Element of bool (bool the carrier of [:SS,S:])
the carrier of [:SS,S:] is non empty set
bool the carrier of [:SS,S:] is non empty set
bool (bool the carrier of [:SS,S:]) is non empty set
Wy is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
the carrier of Wy is non empty set
the topology of Wy is non empty Element of bool (bool the carrier of Wy)
bool the carrier of Wy is non empty set
bool (bool the carrier of Wy) is non empty set
TopStruct(# the carrier of Wy, the topology of Wy #) is non empty strict TopSpace-like monotone-convergence TopStruct
TopStruct(# the carrier of [:SS,S:], the topology of [:SS,S:] #) is non empty strict TopSpace-like TopStruct
L is non empty RelStr
the carrier of L is non empty set
S is non empty 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 non empty RelStr
the carrier of S is non empty set
[: 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 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 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 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 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 is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
Wy " is Relation-like Function-like set
proj2 (Wy ") is set
T is set
WY is set
[T,WY] is non empty set
{T,WY} is finite set
{T} is trivial finite set
{{T,WY},{T}} is finite V45() set
T1 is Element of the carrier of S
wy is Element of the carrier of S
Wy . T1 is Element of the carrier of S
Wy . wy is Element of the carrier of S
x is Element of the carrier of L
y is Element of the carrier of L
T is set
WY is set
[T,WY] is non empty set
{T,WY} is finite set
{T} is trivial finite set
{{T,WY},{T}} is finite V45() set
T1 is Element of the carrier of L
wy is Element of the carrier of L
SS . T1 is Element of the carrier of S
SS . wy is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
Scott-Convergence L is (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric non void RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:SS,S:] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:SS,S:] is non empty Element of bool (bool the carrier of [:SS,S:])
the carrier of [:SS,S:] is non empty set
bool the carrier of [:SS,S:] is non empty set
bool (bool the carrier of [:SS,S:]) is non empty set
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 non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) 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
UPS (L,(BoolePoset 1)) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(BoolePoset 1) |^ the carrier of L is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(UPS (L,(BoolePoset 1))) |^ the carrier of S is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
((BoolePoset 1) |^ the carrier of L) |^ the carrier of S is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
UPS (S,(UPS (L,(BoolePoset 1)))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (UPS (L,(BoolePoset 1))) is functional non empty set
the carrier of (InclPoset (sigma L)) is non empty set
[: the carrier of (UPS (L,(BoolePoset 1))), the carrier of (InclPoset (sigma L)):] is non empty set
bool [: the carrier of (UPS (L,(BoolePoset 1))), the carrier of (InclPoset (sigma L)):] is non empty set
[: the carrier of L, the carrier of (BoolePoset 1):] is non empty set
bool [: the carrier of L, the carrier of (BoolePoset 1):] is non empty set
Wy is Relation-like the carrier of (UPS (L,(BoolePoset 1))) -defined the carrier of (InclPoset (sigma L)) -valued Function-like non empty V24( the carrier of (UPS (L,(BoolePoset 1)))) quasi_total Element of bool [: the carrier of (UPS (L,(BoolePoset 1))), the carrier of (InclPoset (sigma L)):]
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total onto bijective monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic V376(S) V377(S) V378(S) Element of bool [: the carrier of S, the carrier of S:]
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
UPS ((id S),Wy) is Relation-like the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))) -defined the carrier of (UPS (S,(InclPoset (sigma L)))) -valued Function-like non empty V24( the carrier of (UPS (S,(UPS (L,(BoolePoset 1)))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS (S,(InclPoset (sigma L)))):]
the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))) is functional non empty set
UPS (S,(InclPoset (sigma L))) is non empty V185() strict reflexive transitive antisymmetric non void RelStr
the carrier of (UPS (S,(InclPoset (sigma L)))) is functional non empty set
[: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
bool [: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
UPS ([:S,L:],(BoolePoset 1)) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (UPS ([:S,L:],(BoolePoset 1))) is functional non empty set
[: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS ([:S,L:],(BoolePoset 1))):] is non empty set
bool [: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS ([:S,L:],(BoolePoset 1))):] is non empty set
WY is Relation-like the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))) -defined the carrier of (UPS ([:S,L:],(BoolePoset 1))) -valued Function-like non empty V24( the carrier of (UPS (S,(UPS (L,(BoolePoset 1)))))) quasi_total Function-yielding V40() Element of bool [: the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))), the carrier of (UPS ([:S,L:],(BoolePoset 1))):]
WY " is Relation-like the carrier of (UPS ([:S,L:],(BoolePoset 1))) -defined the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))) -valued Function-like non empty V24( the carrier of (UPS ([:S,L:],(BoolePoset 1)))) quasi_total Function-yielding V40() Element of bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))):]
[: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))):] is non empty set
bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(UPS (L,(BoolePoset 1))))):] is non empty set
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
InclPoset the topology of S is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
((InclPoset the topology of S)) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of S
InclPoset (sigma [:S,L:]) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (sigma [:S,L:])) is non empty set
[: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (InclPoset (sigma [:S,L:])):] is non empty set
bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (InclPoset (sigma [:S,L:])):] is non empty set
[: the carrier of [:S,L:], the carrier of (BoolePoset 1):] is non empty set
bool [: the carrier of [:S,L:], the carrier of (BoolePoset 1):] is non empty set
x is Relation-like the carrier of (UPS ([:S,L:],(BoolePoset 1))) -defined the carrier of (InclPoset (sigma [:S,L:])) -valued Function-like non empty V24( the carrier of (UPS ([:S,L:],(BoolePoset 1)))) quasi_total Element of bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (InclPoset (sigma [:S,L:])):]
x " is Relation-like the carrier of (InclPoset (sigma [:S,L:])) -defined the carrier of (UPS ([:S,L:],(BoolePoset 1))) -valued Function-like non empty V24( the carrier of (InclPoset (sigma [:S,L:]))) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS ([:S,L:],(BoolePoset 1))):]
[: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS ([:S,L:],(BoolePoset 1))):] is non empty set
bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS ([:S,L:],(BoolePoset 1))):] is non empty set
(UPS ((id S),Wy)) * (WY ") is Relation-like the carrier of (UPS ([:S,L:],(BoolePoset 1))) -defined the carrier of (UPS (S,(InclPoset (sigma L)))) -valued Function-like non empty V24( the carrier of (UPS ([:S,L:],(BoolePoset 1)))) quasi_total Function-yielding V40() Element of bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(InclPoset (sigma L)))):]
[: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
bool [: the carrier of (UPS ([:S,L:],(BoolePoset 1))), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
((UPS ((id S),Wy)) * (WY ")) * (x ") is Relation-like the carrier of (InclPoset (sigma [:S,L:])) -defined the carrier of (UPS (S,(InclPoset (sigma L)))) -valued Function-like non empty V24( the carrier of (InclPoset (sigma [:S,L:]))) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS (S,(InclPoset (sigma L)))):]
[: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (UPS (S,(InclPoset (sigma L)))):] is non empty set
the carrier of ((InclPoset the topology of S)) is non empty set
the InternalRel of ((InclPoset the topology of S)) is Relation-like the carrier of ((InclPoset the topology of S)) -defined the carrier of ((InclPoset the topology of S)) -valued non empty Element of bool [: the carrier of ((InclPoset the topology of S)), the carrier of ((InclPoset the topology of S)):]
[: the carrier of ((InclPoset the topology of S)), the carrier of ((InclPoset the topology of S)):] is non empty set
bool [: the carrier of ((InclPoset the topology of S)), the carrier of ((InclPoset the topology of S)):] is non empty set
RelStr(# the carrier of ((InclPoset the topology of S)), the InternalRel of ((InclPoset the topology of S)) #) is strict RelStr
the InternalRel of (InclPoset (sigma L)) is Relation-like the carrier of (InclPoset (sigma L)) -defined the carrier of (InclPoset (sigma L)) -valued non empty Element of bool [: the carrier of (InclPoset (sigma L)), the carrier of (InclPoset (sigma L)):]
[: the carrier of (InclPoset (sigma L)), the carrier of (InclPoset (sigma L)):] is non empty set
bool [: the carrier of (InclPoset (sigma L)), the carrier of (InclPoset (sigma L)):] is non empty set
RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #) is strict RelStr
ContMaps (SS,((InclPoset the topology of S))) is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (ContMaps (SS,((InclPoset the topology of S)))) is functional non empty set
x2 is set
[: the carrier of SS, the carrier of ((InclPoset the topology of S)):] is non empty set
bool [: the carrier of SS, the carrier of ((InclPoset the topology of S)):] is non empty set
[: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
bool [: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
u2 is Relation-like the carrier of SS -defined the carrier of ((InclPoset the topology of S)) -valued Function-like non empty V24( the carrier of SS) quasi_total Element of bool [: the carrier of SS, the carrier of ((InclPoset the topology of S)):]
x2 is set
[: the carrier of SS, the carrier of ((InclPoset the topology of S)):] is non empty set
bool [: the carrier of SS, the carrier of ((InclPoset the topology of S)):] is non empty set
u2 is Relation-like the carrier of SS -defined the carrier of ((InclPoset the topology of S)) -valued Function-like non empty V24( the carrier of SS) quasi_total Element of bool [: the carrier of SS, the carrier of ((InclPoset the topology of S)):]
[: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
bool [: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
u1 is Relation-like the carrier of S -defined the carrier of (InclPoset (sigma L)) -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of (InclPoset (sigma L)):]
[: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (ContMaps (SS,((InclPoset the topology of S)))):] is non empty set
bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (ContMaps (SS,((InclPoset the topology of S)))):] is non empty set
(SS,S) is Relation-like the carrier of (InclPoset the topology of [:SS,S:]) -defined the carrier of (ContMaps (SS,((InclPoset the topology of S)))) -valued Function-like non empty V24( the carrier of (InclPoset the topology of [:SS,S:])) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset the topology of [:SS,S:]), the carrier of (ContMaps (SS,((InclPoset the topology of S)))):]
InclPoset the topology of [:SS,S:] is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
the carrier of (InclPoset the topology of [:SS,S:]) is non empty non trivial set
[: the carrier of (InclPoset the topology of [:SS,S:]), the carrier of (ContMaps (SS,((InclPoset the topology of S)))):] is non empty set
bool [: the carrier of (InclPoset the topology of [:SS,S:]), the carrier of (ContMaps (SS,((InclPoset the topology 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 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
(BoolePoset 1) |^ the carrier of [:S,L:] is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[: the carrier of S, the carrier of L:] is non empty set
(BoolePoset 1) |^ [: the carrier of S, the carrier of L:] is non empty V185() strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
x2 is Relation-like the carrier of (InclPoset (sigma [:S,L:])) -defined the carrier of (ContMaps (SS,((InclPoset the topology of S)))) -valued Function-like non empty V24( the carrier of (InclPoset (sigma [:S,L:]))) quasi_total Function-yielding V40() Element of bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (ContMaps (SS,((InclPoset the topology of S)))):]
u1 is Element of the carrier of (InclPoset (sigma [:S,L:]))
x2 . u1 is Relation-like Function-like Element of the carrier of (ContMaps (SS,((InclPoset the topology of S))))
y1 is Element of the carrier of S
(x2 . u1) . y1 is set
{ b1 where b1 is Element of the carrier of L : [y1,b1] in u1 } is set
[: the carrier of S, the carrier of (UPS (L,(BoolePoset 1))):] is non empty set
bool [: the carrier of S, the carrier of (UPS (L,(BoolePoset 1))):] is non empty set
(x ") . u1 is Relation-like Function-like Element of the carrier of (UPS ([:S,L:],(BoolePoset 1)))
(WY ") . ((x ") . u1) is Relation-like Function-like Element of the carrier of (UPS (S,(UPS (L,(BoolePoset 1)))))
y2 is Relation-like the carrier of S -defined the carrier of (UPS (L,(BoolePoset 1))) -valued Function-like non empty V24( the carrier of S) quasi_total Function-yielding V40() directed-sups-preserving Element of bool [: the carrier of S, the carrier of (UPS (L,(BoolePoset 1))):]
Wy * y2 is Relation-like the carrier of S -defined the carrier of (InclPoset (sigma L)) -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of (InclPoset (sigma L)):]
[: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
bool [: the carrier of S, the carrier of (InclPoset (sigma L)):] is non empty set
(Wy * y2) * (id the carrier of S) is Relation-like the carrier of S -defined the carrier of (InclPoset (sigma L)) -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of (InclPoset (sigma L)):]
((WY ") . ((x ") . u1)) . y1 is Relation-like Function-like Element of the carrier of (UPS (L,(BoolePoset 1)))
proj1 (((WY ") . ((x ") . u1)) . y1) is set
((UPS ((id S),Wy)) * (WY ")) . ((x ") . u1) is Relation-like Function-like Element of the carrier of (UPS (S,(InclPoset (sigma L))))
(UPS ((id S),Wy)) . ((WY ") . ((x ") . u1)) is Relation-like Function-like Element of the carrier of (UPS (S,(InclPoset (sigma L))))
y2 . y1 is Relation-like Function-like Element of the carrier of (UPS (L,(BoolePoset 1)))
Wy . (y2 . y1) is Element of the carrier of (InclPoset (sigma L))
(((WY ") . ((x ") . u1)) . y1) " {1} is set
rng x is Element of bool the carrier of (InclPoset (sigma [:S,L:]))
bool the carrier of (InclPoset (sigma [:S,L:])) is non empty set
[#] (InclPoset (sigma [:S,L:])) is non empty non proper lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of (InclPoset (sigma [:S,L:]))
dom (WY ") is functional Element of bool the carrier of (UPS ([:S,L:],(BoolePoset 1)))
bool the carrier of (UPS ([:S,L:],(BoolePoset 1))) is non empty set
curry ((x ") . u1) is Relation-like Function-like set
id (rng x) is Relation-like rng x -defined rng x -valued Function-like one-to-one V24( rng x) quasi_total Element of bool [:(rng x),(rng x):]
[:(rng x),(rng x):] is set
bool [:(rng x),(rng x):] is non empty set
(id (rng x)) . u1 is set
x * (x ") is Relation-like the carrier of (InclPoset (sigma [:S,L:])) -defined the carrier of (InclPoset (sigma [:S,L:])) -valued Function-like non empty V24( the carrier of (InclPoset (sigma [:S,L:]))) quasi_total Element of bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (InclPoset (sigma [:S,L:])):]
[: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (InclPoset (sigma [:S,L:])):] is non empty set
bool [: the carrier of (InclPoset (sigma [:S,L:])), the carrier of (InclPoset (sigma [:S,L:])):] is non empty set
(x * (x ")) . u1 is Element of the carrier of (InclPoset (sigma [:S,L:]))
x . ((x ") . u1) is Element of the carrier of (InclPoset (sigma [:S,L:]))
y1 is Relation-like the carrier of [:S,L:] -defined the carrier of (BoolePoset 1) -valued Function-like non empty V24( the carrier of [:S,L:]) quasi_total directed-sups-preserving Element of bool [: the carrier of [:S,L:], the carrier of (BoolePoset 1):]
y1 " {1} is Element of bool the carrier of [:S,L:]
y2 is set
(((WY ") . ((x ") . u1)) . y1) . y2 is set
v2 is Element of the carrier of L
(((WY ") . ((x ") . u1)) . y1) . v2 is Element of the carrier of (BoolePoset 1)
dom y1 is Element of bool the carrier of [:S,L:]
[y1,v2] is non empty Element of the carrier of [:S,L:]
{y1,v2} is finite set
{y1} is trivial finite set
{{y1,v2},{y1}} is finite V45() set
proj1 ((x ") . u1) is set
((x ") . u1) . (y1,v2) is set
[y1,v2] is non empty set
((x ") . u1) . [y1,v2] is set
((x ") . u1) " {1} is set
y2 is set
v2 is Element of the carrier of L
[y1,v2] is non empty Element of the carrier of [:S,L:]
{y1,v2} is finite set
{y1} is trivial finite set
{{y1,v2},{y1}} is finite V45() set
dom y1 is Element of bool the carrier of [:S,L:]
proj1 ((x ") . u1) is set
(curry ((x ") . u1)) . y1 is set
((x ") . u1) . (y1,v2) is set
[y1,v2] is non empty set
((x ") . u1) . [y1,v2] is set
v1 is Relation-like Function-like set
v1 . v2 is set
(((WY ") . ((x ") . u1)) . y1) . v2 is Element of the carrier of (BoolePoset 1)
y1 is Element of the carrier of S
u1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of S
the carrier of u1 is non empty set
bool the carrier of u1 is non empty set
y2 is non empty open upper inaccessible_by_directed_joins a_neighborhood of y1
u1 is non empty TopSpace-like TopStruct
the carrier of u1 is non empty set
y1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of S
the carrier of y1 is non empty set
[: the carrier of u1, the carrier of y1:] is non empty set
bool [: the carrier of u1, the carrier of y1:] is non empty set
y2 is Relation-like the carrier of u1 -defined the carrier of y1 -valued Function-like non empty V24( the carrier of u1) quasi_total continuous Element of bool [: the carrier of u1, the carrier of y1:]
*graph y2 is Relation-like set
[:u1,S:] is non empty strict TopSpace-like TopStruct
the carrier of [:u1,S:] is non empty set
bool the carrier of [:u1,S:] is non empty set
u1 is set
rng (SS,S) is functional Element of bool the carrier of (ContMaps (SS,((InclPoset the topology of S))))
bool the carrier of (ContMaps (SS,((InclPoset the topology of S)))) is non empty set
dom (SS,S) is Element of bool the carrier of (InclPoset the topology of [:SS,S:])
bool the carrier of (InclPoset the topology of [:SS,S:]) is non empty set
y1 is Element of the carrier of (InclPoset (sigma [:S,L:]))
x2 . y1 is Relation-like Function-like Element of the carrier of (ContMaps (SS,((InclPoset the topology of S))))
y2 is set
(SS,S) . y2 is Relation-like Function-like set
y1 is Element of the carrier of (InclPoset the topology of [:SS,S:])
v2 is set
v1 is set
e is set
[v1,e] is non empty set
{v1,e} is finite set
{v1} is trivial finite set
{{v1,e},{v1}} is finite V45() set
Y is Element of the carrier of L
e is Element of the carrier of S
{ b1 where b1 is Element of the carrier of L : [e,b1] in u1 } is set
(x2 . y1) . e is set
y2 is Relation-like open Element of bool the carrier of [:SS,S:]
(y2, the carrier of S) *graph is Relation-like Function-like set
((y2, the carrier of S) *graph) . e is set
Im (y2,e) is set
{e} is trivial finite set
y2 .: {e} is set
DD is set
[DD,Y] is non empty set
{DD,Y} is finite set
{DD} is trivial finite set
{{DD,Y},{DD}} is finite V45() set
v2 is set
y2 is Relation-like open Element of bool the carrier of [:SS,S:]
[: the carrier of SS, the carrier of S:] is non empty set
v1 is set
e is set
[v1,e] is non empty set
{v1,e} is finite set
{v1} is trivial finite set
{{v1,e},{v1}} is finite V45() set
e is Element of the carrier of S
{e} is trivial finite set
Y is Element of the carrier of L
Im (y2,e) is set
y2 .: {e} is set
(y2, the carrier of S) *graph is Relation-like Function-like set
((y2, the carrier of S) *graph) . e is set
(SS,S) . y1 is Relation-like Function-like Element of the carrier of (ContMaps (SS,((InclPoset the topology of S))))
((SS,S) . y1) . e is set
{ b1 where b1 is Element of the carrier of L : [e,b1] in u1 } is set
DD is Element of the carrier of L
[e,DD] is non empty Element of the carrier of [:S,L:]
{e,DD} is finite set
{{e,DD},{e}} is finite V45() set
u1 is set
y1 is Element of the carrier of (InclPoset the topology of [:SS,S:])
rng x2 is functional Element of bool the carrier of (ContMaps (SS,((InclPoset the topology of S))))
bool the carrier of (ContMaps (SS,((InclPoset the topology of S)))) is non empty set
dom x2 is Element of bool the carrier of (InclPoset (sigma [:S,L:]))
bool the carrier of (InclPoset (sigma [:S,L:])) is non empty set
(SS,S) . y1 is Relation-like Function-like Element of the carrier of (ContMaps (SS,((InclPoset the topology of S))))
y1 is set
x2 . y1 is Relation-like Function-like set
y2 is Element of the carrier of (InclPoset (sigma [:S,L:]))
v2 is set
v1 is set
e is set
[v1,e] is non empty set
{v1,e} is finite set
{v1} is trivial finite set
{{v1,e},{v1}} is finite V45() set
Y is Element of the carrier of L
e is Element of the carrier of S
{ b1 where b1 is Element of the carrier of L : [e,b1] in y2 } is set
x2 . y2 is Relation-like Function-like Element of the carrier of (ContMaps (SS,((InclPoset the topology of S))))
(x2 . y2) . e is set
y2 is Relation-like open Element of bool the carrier of [:SS,S:]
(y2, the carrier of S) *graph is Relation-like Function-like set
((y2, the carrier of S) *graph) . e is set
Im (y2,e) is set
{e} is trivial finite set
y2 .: {e} is set
DD is set
[DD,Y] is non empty set
{DD,Y} is finite set
{DD} is trivial finite set
{{DD,Y},{DD}} is finite V45() set
v2 is set
y2 is Relation-like open Element of bool the carrier of [:SS,S:]
[: the carrier of SS, the carrier of S:] is non empty set
v1 is set
e is set
[v1,e] is non empty set
{v1,e} is finite set
{v1} is trivial finite set
{{v1,e},{v1}} is finite V45() set
e is Element of the carrier of S
{e} is trivial finite set
Y is Element of the carrier of L
Im (y2,e) is set
y2 .: {e} is set
(y2, the carrier of S) *graph is Relation-like Function-like set
((y2, the carrier of S) *graph) . e is set
((SS,S) . y1) . e is set
{ b1 where b1 is Element of the carrier of L : [e,b1] in y2 } is set
DD is Element of the carrier of L
[e,DD] is non empty Element of the carrier of [:S,L:]
{e,DD} is finite set
{{e,DD},{e}} is finite V45() set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
Scott-Convergence L is (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric non void RelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L -valued non empty Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation 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 topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L #) is non empty strict TopSpace-like monotone-convergence TopStruct
Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is (CONSTANTS) (SUBNETS) Convergence-Class of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is strict TopStruct
sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)
the topology of (ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)))
the carrier of (ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L))) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete distributive RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete 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 non void monotone-convergence with_suprema with_infima complete TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
[: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty strict TopSpace-like T_0 TopStruct
the topology of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty Element of bool (bool the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:])
the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
bool the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
bool (bool the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:]) is non empty set
{ [b1,b2] where b1 is open Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L, b2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L : b2 in b1 } is set
T is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[:T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
bool the carrier of [:T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
WY is set
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued non empty Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty 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
the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is non empty non trivial set
the InternalRel of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is Relation-like the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) -defined the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):]
[: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):] is non empty set
bool [: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the InternalRel of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) #) is strict RelStr
T1 is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
wy is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[T1,wy] is non empty set
{T1,wy} is finite set
{T1} is trivial finite set
{{T1,wy},{T1}} is finite V45() set
[: the carrier of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S -valued non empty Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S #) is strict RelStr
the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is non empty non trivial set
the InternalRel of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is Relation-like the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) -defined the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) -valued non empty Element of bool [: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):]
[: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):] is non empty set
bool [: the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L):] is non empty set
RelStr(# the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L), the InternalRel of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) #) is strict RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued non empty Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty 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
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 T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
WY is Relation-like Element of bool the carrier of [:T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:]
wy is Element of bool the carrier of [:S,L:]
x is non empty directed Element of bool the carrier of [:S,L:]
"\/" (x,[:S,L:]) is Element of the carrier of [:S,L:]
proj1 x is Element of bool the carrier of S
bool the carrier of S is non empty set
"\/" ((proj1 x),S) is Element of the carrier of S
proj2 x is Element of bool the carrier of L
"\/" ((proj2 x),L) is Element of the carrier of L
[("\/" ((proj1 x),S)),("\/" ((proj2 x),L))] is non empty Element of the carrier of [:S,L:]
{("\/" ((proj1 x),S)),("\/" ((proj2 x),L))} is finite set
{("\/" ((proj1 x),S))} is trivial finite set
{{("\/" ((proj1 x),S)),("\/" ((proj2 x),L))},{("\/" ((proj1 x),S))}} is finite V45() set
y is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
x1 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[y,x1] is non empty set
{y,x1} is finite set
{y} is trivial finite set
{{y,x1},{y}} is finite V45() set
x2 is Element of bool the carrier of L
bool the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L) is non empty set
u1 is Element of bool the carrier of (InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L)
union u1 is set
y1 is non empty directed Element of bool the carrier of L
"\/" (y1,L) is Element of the carrier of L
u2 is upper inaccessible_by_directed_joins Element of bool the carrier of L
y2 is set
y1 is Element of the carrier of L
y2 is set
v2 is set
[v2,y1] is non empty set
{v2,y1} is finite set
{v2} is trivial finite set
{{v2,y1},{v2}} is finite V45() set
v1 is Element of the carrier of S
e is set
[v1,e] is non empty set
{v1,e} is finite set
{v1} is trivial finite set
{{v1,e},{v1}} is finite V45() set
e is Element of the carrier of L
[v1,e] is non empty Element of the carrier of [:S,L:]
{v1,e} is finite set
{{v1,e},{v1}} is finite V45() set
Y is Element of the carrier of S
[Y,y1] is non empty Element of the carrier of [:S,L:]
{Y,y1} is finite set
{Y} is trivial finite set
{{Y,y1},{Y}} is finite V45() set
DD is Element of the carrier of [:S,L:]
[: the carrier of S, the carrier of L:] is non empty set
DD1 is set
DD2 is set
[DD1,DD2] is non empty set
{DD1,DD2} is finite set
{DD1} is trivial finite set
{{DD1,DD2},{DD1}} is finite V45() set
DD1 is Element of the carrier of S
DD2 is Element of the carrier of L
[DD1,DD2] is non empty Element of the carrier of [:S,L:]
{DD1,DD2} is finite set
{DD1} is trivial finite set
{{DD1,DD2},{DD1}} is finite V45() set
DD1 is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
DD2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[DD1,DD2] is non empty set
{DD1,DD2} is finite set
{DD1} is trivial finite set
{{DD1,DD2},{DD1}} is finite V45() set
x is Element of the carrier of [:S,L:]
y is Element of the carrier of [:S,L:]
x1 is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
x2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[x1,x2] is non empty set
{x1,x2} is finite set
{x1} is trivial finite set
{{x1,x2},{x1}} is finite V45() set
[: the carrier of S, the carrier of L:] is non empty set
y1 is set
y2 is set
[y1,y2] is non empty set
{y1,y2} is finite set
{y1} is trivial finite set
{{y1,y2},{y1}} is finite V45() set
y2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
y1 is open upper inaccessible_by_directed_joins Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
u1 is Element of the carrier of S
u2 is Element of the carrier of L
[u1,u2] is non empty Element of the carrier of [:S,L:]
{u1,u2} is finite set
{u1} is trivial finite set
{{u1,u2},{u1}} is finite V45() set
v1 is Element of the carrier of S
v2 is Element of the carrier of L
[v1,v2] is non empty Element of the carrier of [:S,L:]
{v1,v2} is finite set
{v1} is trivial finite set
{{v1,v2},{v1}} is finite V45() set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S) is non empty set
sigma 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
Scott-Convergence S is (CONSTANTS) (SUBNETS) Convergence-Class of S
ConvergenceSpace (Scott-Convergence S) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence S)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence S)))
the carrier of (ConvergenceSpace (Scott-Convergence S)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence S)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence S))) is non empty set
T1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
the topology of T1 is non empty Element of bool (bool the carrier of T1)
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S, the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S #) is non empty strict TopSpace-like monotone-convergence TopStruct
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like monotone-convergence TopStruct
T is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
Wy is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
the carrier of Wy is non empty set
bool the carrier of Wy is non empty set
WY is non empty open upper inaccessible_by_directed_joins a_neighborhood of T
Wy is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
[:Wy, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty strict TopSpace-like T_0 TopStruct
the carrier of [:Wy, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
bool the carrier of [:Wy, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L:] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
Scott-Convergence L is (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric non void RelStr
(L) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:(S),(L):] is non empty Element of bool (bool the carrier of [:(S),(L):])
the carrier of [:(S),(L):] is non empty set
bool the carrier of [:(S),(L):] is non empty set
bool (bool the carrier of [:(S),(L):]) is non empty set
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete 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 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 (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 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 monotone-convergence TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
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 non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) 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 TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete 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 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 non empty strict TopSpace-like monotone-convergence TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
[:SS,S:] is non empty strict TopSpace-like T_0 TopStruct
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
the topology of [:SS,S:] is non empty Element of bool (bool the carrier of [:SS,S:])
the carrier of [:SS,S:] is non empty set
bool the carrier of [:SS,S:] is non empty set
bool (bool the carrier of [:SS,S:]) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(L) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
SS is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:SS,S:] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:SS,S:] is non empty Element of bool (bool the carrier of [:SS,S:])
the carrier of [:SS,S:] is non empty set
bool the carrier of [:SS,S:] is non empty set
bool (bool the carrier of [:SS,S:]) is non empty set
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 (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 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 monotone-convergence TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
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 non empty 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
RelStr(# the carrier of SS, the InternalRel of SS #) 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 TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete 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 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 non empty strict TopSpace-like monotone-convergence TopStruct
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 non empty strict TopSpace-like monotone-convergence TopStruct
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
([:S,L:]) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
the carrier of ([:S,L:]) is non empty set
the topology of ([:S,L:]) is non empty Element of bool (bool the carrier of ([:S,L:]))
bool the carrier of ([:S,L:]) is non empty set
bool (bool the carrier of ([:S,L:])) is non empty set
TopStruct(# the carrier of ([:S,L:]), the topology of ([:S,L:]) #) is non empty strict TopSpace-like monotone-convergence TopStruct
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:(S),(L):] is non empty Element of bool (bool the carrier of [:(S),(L):])
the carrier of [:(S),(L):] is non empty set
bool the carrier of [:(S),(L):] is non empty set
bool (bool the carrier of [:(S),(L):]) is non empty set
([:S,L:]) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
the carrier of ([:S,L:]) is non empty set
the topology of ([:S,L:]) is non empty Element of bool (bool the carrier of ([:S,L:]))
bool the carrier of ([:S,L:]) is non empty set
bool (bool the carrier of ([:S,L:])) is non empty set
TopStruct(# the carrier of ([:S,L:]), the topology of ([:S,L:]) #) is non empty strict TopSpace-like monotone-convergence TopStruct
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
(L) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
([:S,L:]) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
the carrier of ([:S,L:]) is non empty set
the topology of ([:S,L:]) is non empty Element of bool (bool the carrier of ([:S,L:]))
bool the carrier of ([:S,L:]) is non empty set
bool (bool the carrier of ([:S,L:])) is non empty set
TopStruct(# the carrier of ([:S,L:]), the topology of ([:S,L:]) #) is non empty strict TopSpace-like monotone-convergence TopStruct
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
Omega ([:S,L:]) is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict non void with_suprema with_infima complete TopRelStr
Omega [:(S),(L):] is non empty TopSpace-like reflexive transitive antisymmetric strict non void TopRelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:(S),(L):] is non empty Element of bool (bool the carrier of [:(S),(L):])
the carrier of [:(S),(L):] is non empty set
bool the carrier of [:(S),(L):] is non empty set
bool (bool the carrier of [:(S),(L):]) is non empty set
([:S,L:]) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
Omega [:(S),(L):] is non empty TopSpace-like reflexive transitive antisymmetric strict non void TopRelStr
the carrier of ([:S,L:]) is non empty set
the topology of ([:S,L:]) is non empty Element of bool (bool the carrier of ([:S,L:]))
bool the carrier of ([:S,L:]) is non empty set
bool (bool the carrier of ([:S,L:])) is non empty set
TopStruct(# the carrier of ([:S,L:]), the topology of ([:S,L:]) #) is non empty strict TopSpace-like monotone-convergence TopStruct
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
Scott-Convergence L is (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric non void RelStr
(L) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of L
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:(S),(L):] is non empty Element of bool (bool the carrier of [:(S),(L):])
the carrier of [:(S),(L):] is non empty set
bool the carrier of [:(S),(L):] is non empty set
bool (bool the carrier of [:(S),(L):]) is non empty set
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
([:S,L:]) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of [:S,L:]
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
Omega [:(S),(L):] is non empty TopSpace-like reflexive transitive antisymmetric strict non void TopRelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
[:S,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete non void with_suprema with_infima complete RelStr
sigma [:S,L:] is non empty Element of bool (bool the carrier of [:S,L:])
the carrier of [:S,L:] is non empty set
bool the carrier of [:S,L:] is non empty set
bool (bool the carrier of [:S,L:]) is non empty set
Scott-Convergence [:S,L:] is (CONSTANTS) (SUBNETS) Convergence-Class of [:S,L:]
ConvergenceSpace (Scott-Convergence [:S,L:]) is strict TopStruct
the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])))
the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is set
bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:])) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence [:S,L:]))) is non empty set
(S) is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V271() up-complete /\-complete strict Scott non void monotone-convergence with_suprema with_infima complete TopAugmentation of S
[:(S),(L):] is non empty strict TopSpace-like T_0 TopStruct
the topology of [:(S),(L):] is non empty Element of bool (bool the carrier of [:(S),(L):])
the carrier of [:(S),(L):] is non empty set
bool the carrier of [:(S),(L):] is non empty set
bool (bool the carrier of [:(S),(L):]) is non empty set