:: WAYBEL30 semantic presentation

K149() is non trivial V23() non finite cardinal limit_cardinal Element of bool K145()
K145() is set
bool K145() is non empty set
K87() is non trivial V23() non finite cardinal limit_cardinal set
bool K87() is non empty non trivial non finite set
{} is empty V23() V27() finite V32() cardinal {} -element set
the empty V23() V27() finite V32() cardinal {} -element set is empty V23() V27() finite V32() cardinal {} -element set
1 is non empty set
{{},1} is non empty finite set
bool K149() is non empty non trivial non finite set
K462() is non empty strict TopSpace-like TopStruct
the carrier of K462() is non empty set
K510() is set
{{}} is non empty trivial finite V32() 1 -element set
K467({{}}) is M44({{}})
[:K467({{}}),{{}}:] is set
bool [:K467({{}}),{{}}:] is non empty set
PFuncs (K467({{}}),{{}}) is set
K559() is strict TopStruct
N is set
S is non empty set
union S is set
N /\ (union S) is set
{ (N /\ b₁) where b₁ is Element of S : verum } is set
union { (N /\ b₁) where b₁ is Element of S : verum } is set
T is set
y is set
N /\ y is set
T is set
y is set
BC is Element of S
N /\ BC is set
N is non empty reflexive transitive non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
S is non empty directed Element of bool the carrier of (InclPoset (Ids N))
union S is set
the Element of S is Element of S
bool the carrier of N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
y is set
BC is non empty directed lower Element of bool the carrier of N
y is non empty directed lower Element of bool the carrier of N
BC is Element of bool the carrier of N
BC is non empty directed lower Element of bool the carrier of N
BC is Element of bool the carrier of N
BC is Element of bool the carrier of N
BC \/ BC is Element of bool the carrier of N
A is Element of the carrier of (InclPoset (Ids N))
C is Element of the carrier of (InclPoset (Ids N))
c₉ is Element of the carrier of (InclPoset (Ids N))
KK is non empty directed lower Element of bool the carrier of N
K is Element of bool the carrier of N
BC is Element of bool the carrier of N
BC is non empty directed lower Element of bool the carrier of N
the Element of y is Element of y
N is non empty reflexive transitive non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
T is Element of the carrier of (InclPoset (Ids N))
S is non empty directed Element of bool the carrier of (InclPoset (Ids N))
union S is set
y is Element of the carrier of (InclPoset (Ids N))
BC is set
N is non empty reflexive transitive non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
T is Element of the carrier of (InclPoset (Ids N))
S is non empty directed Element of bool the carrier of (InclPoset (Ids N))
union S is set
y is Element of the carrier of (InclPoset (Ids N))
BC is set
BC is set
A is Element of the carrier of (InclPoset (Ids N))
N is non empty reflexive transitive non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
T is non empty directed Element of bool the carrier of (InclPoset (Ids N))
union T is set
y is non empty directed lower Element of bool the carrier of N
BC is Element of the carrier of (InclPoset (Ids N))
BC is Element of the carrier of (InclPoset (Ids N))
N is non empty reflexive transitive non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
S is non empty directed Element of bool the carrier of (InclPoset (Ids N))
"\/" (S,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
union S is set
T is non empty directed lower Element of bool the carrier of N
y is Element of the carrier of (InclPoset (Ids N))
BC is Element of the carrier of (InclPoset (Ids N))
N is non empty reflexive transitive antisymmetric with_infima non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete with_infima non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
S is non empty directed Element of bool the carrier of (InclPoset (Ids N))
T is Element of the carrier of (InclPoset (Ids N))
{T} is non empty trivial finite 1 -element Element of bool the carrier of (InclPoset (Ids N))
{T} "/\" S is non empty Element of bool the carrier of (InclPoset (Ids N))
"\/" (({T} "/\" S),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
{ (T /\ b₁) where b₁ is Element of S : verum } is set
union { (T /\ b₁) where b₁ is Element of S : verum } is set
{ (T "/\" b₁) where b₁ is Element of the carrier of (InclPoset (Ids N)) : b₁ in S } is set
A is set
C is Element of the carrier of (InclPoset (Ids N))
T "/\" C is Element of the carrier of (InclPoset (Ids N))
A is Element of bool the carrier of (InclPoset (Ids N))
"\/" (A,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
"\/" (S,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
T "/\" ("\/" (S,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))
c₉ is set
T /\ ("\/" (S,(InclPoset (Ids N)))) is set
union S is set
K is set
KK is Element of the carrier of (InclPoset (Ids N))
T /\ KK is set
C is set
c₉ is set
K is Element of S
T /\ K is set
KK is Element of the carrier of (InclPoset (Ids N))
T "/\" KK is Element of the carrier of (InclPoset (Ids N))
T /\ KK is set
N is non empty reflexive transitive antisymmetric with_infima non void RelStr
Ids N is non empty set
the carrier of N is non empty set
bool the carrier of N is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of N : verum } is set
InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete with_infima non void RelStr
the carrier of (InclPoset (Ids N)) is non empty set
bool the carrier of (InclPoset (Ids N)) is non empty set
T is Element of the carrier of (InclPoset (Ids N))
{T} is non empty trivial finite 1 -element Element of bool the carrier of (InclPoset (Ids N))
y is non empty directed Element of bool the carrier of (InclPoset (Ids N))
"\/" (y,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
T "/\" ("\/" (y,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))
{T} "/\" y is non empty Element of bool the carrier of (InclPoset (Ids N))
"\/" (({T} "/\" y),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
T "/\" ("\/" (y,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))
T /\ ("\/" (y,(InclPoset (Ids N)))) is set
union y is set
T /\ (union y) is set
{ (T /\ b₁) where b₁ is Element of y : verum } is set
union { (T /\ b₁) where b₁ is Element of y : verum } is set
{T} "/\" y is non empty Element of bool the carrier of (InclPoset (Ids N))
"\/" (({T} "/\" y),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))
N is non empty trivial finite 1 -element RelStr
S is non empty TopAugmentation of N
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
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict RelStr
the carrier of N is non empty trivial finite 1 -element set
the InternalRel of N is Relation-like the carrier of N -defined the carrier of N -valued finite Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty finite set
bool [: the carrier of N, the carrier of N:] is non empty finite V32() set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict RelStr
N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
the carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the topology of N is non empty Element of bool (bool the carrier of N)
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) is strict TopRelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of S is non empty set
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S
the carrier of T is non empty set
the InternalRel of T is non empty 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 non empty set
bool [: the carrier of T, the carrier of T:] 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
TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) is strict TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) 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 Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
the carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the topology of N is non empty Element of bool (bool the carrier of N)
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) is strict TopRelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of S is non empty set
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of S
the carrier of T is non empty set
the InternalRel of T is non empty 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 non empty set
bool [: the carrier of T, the carrier of T:] 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
TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) is strict TopRelStr
omega 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
omega N is Element of bool (bool the carrier of N)
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S) is non empty set
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S \/ the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set
bool the carrier of N is non empty Element of bool (bool the carrier of N)
BC is set
BC is Element of bool (bool the carrier of N)
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)
sigma S is non empty Element of bool (bool the carrier of S)
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
(sigma S) \/ (omega N) is non empty set
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S \/ the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set
A is Element of bool (bool the carrier of N)
FinMeetCl A is Element of bool (bool the carrier of N)
UniCl (FinMeetCl A) is Element of bool (bool the carrier of N)
lambda S is Element of bool (bool the carrier of S)
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of N
y is Element of bool the carrier of S
[#] 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
([#] S) \ y is Element of bool the carrier of S
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
[#] N is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of N
([#] N) \ T is Element of bool the carrier of N
N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
lambda N is Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N
the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N)
the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set
bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete distributive with_suprema with_infima complete non void RelStr
N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty strict reflexive transitive antisymmetric non void RelStr
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty strict reflexive transitive antisymmetric non void RelStr
lambda N is non empty Element of bool (bool the carrier of N)
InclPoset (lambda N) is non empty strict reflexive transitive antisymmetric non void RelStr
the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N
the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N)
the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set
bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete distributive with_suprema with_infima complete non void RelStr
N is non empty reflexive non void RelStr
sigma N is Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
{ (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of bool the carrier of N : ( b₁ in sigma N & b₂ is finite ) } is set
S is set
{} N is empty proper V23() V27() finite V32() cardinal {} -element directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N
uparrow ({} N) is empty proper V23() V27() finite V32() cardinal {} -element directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N
S \ (uparrow ({} N)) is Element of bool S
bool S is non empty set
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
lambda N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
the topology of N is non empty Element of bool (bool the carrier of N)
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
{ (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of bool the carrier of N : ( b₁ in sigma N & b₂ is finite ) } is set
the topology of N is non empty Element of bool (bool the carrier of N)
N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of S is non empty set
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
lambda N is non empty Element of bool (bool the carrier of N)
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
lambda 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
sigma S is non empty Element of bool (bool the carrier of S)
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
omega S is Element of bool (bool the carrier of S)
(sigma S) \/ (omega S) is non empty Element of bool (bool the carrier of S)
FinMeetCl ((sigma S) \/ (omega S)) is Element of bool (bool the carrier of S)
UniCl (FinMeetCl ((sigma S) \/ (omega S))) is Element of bool (bool the carrier of S)
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
omega N is Element of bool (bool the carrier of N)
(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)
FinMeetCl ((sigma N) \/ (omega N)) is Element of bool (bool the carrier of N)
UniCl (FinMeetCl ((sigma N) \/ (omega N))) is Element of bool (bool the carrier of N)
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
S is Element of bool the carrier of N
the topology of N is non empty Element of bool (bool the carrier of N)
N is non empty trivial finite 1 -element reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopRelStr
S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower topological_semilattice satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr
the carrier of S is non empty trivial finite 1 -element set
bool the carrier of S is non empty finite V32() set
T is trivial finite closed directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of S
N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void TopRelStr
the carrier of N is non empty set
S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr
the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty trivial finite 1 -element set
the InternalRel of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty Relation-like the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S -defined the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S -valued finite Element of bool [: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:]
[: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:] is non empty finite set
bool [: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:] is non empty finite V32() set
RelStr(# the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the InternalRel of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_K algebraic arithmetic satisfying_axiom_of_approximation continuous non void RelStr
the topology of S is non empty finite V32() Element of bool (bool the carrier of S)
the carrier of S is non empty trivial finite 1 -element set
bool the carrier of S is non empty finite V32() set
bool (bool the carrier of S) is non empty finite V32() set
{{}, the carrier of S} is non empty finite V32() set
the topology of N is non empty Element of bool (bool the carrier of N)
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
the topology of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty finite V32() Element of bool (bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S)
bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty finite V32() set
bool (bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S) is non empty finite V32() set
lambda N is non empty Element of bool (bool the carrier of N)
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
omega N is Element of bool (bool the carrier of N)
(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)
FinMeetCl ((sigma N) \/ (omega N)) is Element of bool (bool the carrier of N)
UniCl (FinMeetCl ((sigma N) \/ (omega N))) is Element of bool (bool the carrier of N)
(omega N) \/ (sigma N) is non empty Element of bool (bool the carrier of N)
FinMeetCl ((omega N) \/ (sigma N)) is Element of bool (bool the carrier of N)
the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr
the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr
F₁() is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima Scott non void TopRelStr
the carrier of F₁() is non empty set
{ F₃(b₁) where b₁ is Element of the carrier of F₁() : b₁ in {} } is set
N is set
S is Element of the carrier of F₁()
F₃(S) is set
N is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void satisfying_MC meet-continuous RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of bool the carrier of N
uparrow S is upper Element of bool the carrier of N
T is non empty directed Element of bool the carrier of N
"\/" (T,N) is Element of the carrier of N
y is Element of the carrier of N
{y} is non empty trivial finite 1 -element Element of bool the carrier of N
{y} "/\" T is non empty Element of bool the carrier of N
"\/" (({y} "/\" T),N) is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
BC "/\" T is non empty directed Element of bool the carrier of N
BC is Element of the carrier of N
{ (y "/\" b₁) where b₁ is Element of the carrier of N : b₁ in T } is set
A is Element of the carrier of N
y "/\" A is Element of the carrier of N
C is Element of the carrier of N
N is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void satisfying_MC meet-continuous RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is property(S) Element of bool the carrier of N
uparrow S is upper Element of bool the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
sigma 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
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
T is Element of bool the carrier of N
uparrow T is upper Element of bool the carrier of N
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
y is Element of bool the carrier of S
uparrow y is upper Element of bool the carrier of S
BC is Element of bool the carrier of S
the topology of S is non empty Element of bool (bool the carrier of S)
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of N
y is Element of bool the carrier of S
uparrow y is upper Element of bool the carrier of S
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
uparrow T is upper Element of bool the carrier of N
sigma S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
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
T is Element of the carrier of S
y is Element of the carrier of N
BC is non empty open y -quasi_basis Element of bool (bool the carrier of N)
{ (uparrow b₁) where b₁ is Element of bool the carrier of N : b₁ in BC } is set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
bool the carrier of S is non empty Element of bool (bool the carrier of S)
C is set
c₉ is Element of bool the carrier of N
uparrow c₉ is upper Element of bool the carrier of N
C is Element of bool (bool the carrier of S)
c₉ is Element of bool the carrier of S
K is Element of bool the carrier of N
uparrow K is upper Element of bool the carrier of N
KK is Element of bool the carrier of S
uparrow KK is upper Element of bool the carrier of S
the topology of S is non empty Element of bool (bool the carrier of S)
c₉ is set
K is Element of bool the carrier of N
uparrow K is upper Element of bool the carrier of N
Intersect BC is Element of bool the carrier of N
Intersect C is Element of bool the carrier of S
c₉ is Element of bool the carrier of S
uparrow c₉ is upper Element of bool the carrier of S
K is Element of bool the carrier of N
lambda N is non empty Element of bool (bool the carrier of N)
uparrow K is upper Element of bool the carrier of N
sigma S is non empty Element of bool (bool the carrier of S)
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
KK is Element of bool the carrier of N
uparrow KK is upper Element of bool the carrier of N
c₁₂ is Element of bool the carrier of S
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
T is upper Element of bool the carrier of N
Int T is open Element of bool the carrier of N
y is Element of bool the carrier of S
Int y is open Element of bool the carrier of S
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
uparrow (Int T) is upper Element of bool the carrier of N
BC is Element of bool the carrier of S
A is set
uparrow T is upper Element of bool the carrier of N
C is Element of the carrier of N
c₉ is Element of the carrier of N
BC is Element of bool the carrier of S
uparrow BC is upper Element of bool the carrier of S
A is Element of bool the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
T is lower property(S) Element of bool the carrier of N
Cl T is closed Element of bool the carrier of N
y is Element of bool the carrier of S
Cl y is closed Element of bool the carrier of S
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
(Cl T) ` is open Element of bool the carrier of N
T ` is upper closed_under_directed_sups Element of bool the carrier of N
(T `) ` is lower inaccessible_by_directed_joins property(S) Element of bool the carrier of N
Cl ((T `) `) is closed Element of bool the carrier of N
(Cl ((T `) `)) ` is open Element of bool the carrier of N
Int (T `) is open Element of bool the carrier of N
y ` is Element of bool the carrier of S
Int (y `) is open Element of bool the carrier of S
(y `) ` is Element of bool the carrier of S
Cl ((y `) `) is closed Element of bool the carrier of S
(Cl ((y `) `)) ` is open Element of bool the carrier of S
BC is Element of bool the carrier of N
BC ` is Element of bool the carrier of N
N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
sigma 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
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
InclPoset (sigma S) is non empty strict reflexive transitive antisymmetric non void RelStr
[:N,S:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
lambda [:N,S:] is non empty Element of bool (bool the carrier of [:N,S:])
the carrier of [:N,S:] is non empty set
bool the carrier of [:N,S:] is non empty set
bool (bool the carrier of [:N,S:]) is non empty set
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N
y is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of S
[:T,y:] is non empty strict TopSpace-like TopStruct
the topology of [:T,y:] is non empty Element of bool (bool the carrier of [:T,y:])
the carrier of [:T,y:] is non empty set
bool the carrier of [:T,y:] is non empty set
bool (bool the carrier of [:T,y:]) is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of [:N,S:] is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of [:N,S:]
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of [:N,S:] is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of [:N,S:]
the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]
the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty set
the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])
bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] #) is non empty strict TopSpace-like TopStruct
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
omega the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])
sigma the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])
Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is Relation-like V246( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]) V247( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]) M36( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])
K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])))
the carrier of K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])) is non empty set
bool the carrier of K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:],(Scott-Convergence the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]))) is non empty set
(omega the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]) \/ (sigma the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]) is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:])
the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] #) is non empty set
bool the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] #)) is non empty set
the carrier of T is non empty set
the InternalRel of T is non empty 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 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of y is non empty set
the InternalRel of y is non empty Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] is non empty Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] -defined the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]:]
[: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:], the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:] #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of [:N,S:] is non empty Relation-like the carrier of [:N,S:] -defined the carrier of [:N,S:] -valued Element of bool [: the carrier of [:N,S:], the carrier of [:N,S:]:]
[: the carrier of [:N,S:], the carrier of [:N,S:]:] is non empty set
bool [: the carrier of [:N,S:], the carrier of [:N,S:]:] is non empty set
RelStr(# the carrier of [:N,S:], the InternalRel of [:N,S:] #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
[: the carrier of T, the carrier of y:] is non empty set
[: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:] is non empty strict TopSpace-like TopStruct
the topology of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:])
the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void 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 V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:]) is non empty set
omega [:N,S:] is Element of bool (bool the carrier of [:N,S:])
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
Sigma N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Scott non void TopAugmentation of N
the carrier of (Sigma N) is non empty set
the InternalRel of (Sigma N) is non empty Relation-like the carrier of (Sigma N) -defined the carrier of (Sigma N) -valued Element of bool [: the carrier of (Sigma N), the carrier of (Sigma N):]
[: the carrier of (Sigma N), the carrier of (Sigma N):] is non empty set
bool [: the carrier of (Sigma N), the carrier of (Sigma N):] is non empty set
RelStr(# the carrier of (Sigma N), the InternalRel of (Sigma N) #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict TopSpace-like TopStruct
the topology of (Sigma N) is non empty Element of bool (bool the carrier of (Sigma N))
bool the carrier of (Sigma N) is non empty set
bool (bool the carrier of (Sigma N)) is non empty set
TopStruct(# the carrier of (Sigma N), the topology of (Sigma N) #) is non empty strict TopSpace-like TopStruct
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
Sigma S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Scott non void TopAugmentation of S
the carrier of (Sigma S) is non empty set
the InternalRel of (Sigma S) is non empty Relation-like the carrier of (Sigma S) -defined the carrier of (Sigma S) -valued Element of bool [: the carrier of (Sigma S), the carrier of (Sigma S):]
[: the carrier of (Sigma S), the carrier of (Sigma S):] is non empty set
bool [: the carrier of (Sigma S), the carrier of (Sigma S):] is non empty set
RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S #) is non empty strict TopSpace-like TopStruct
the topology of (Sigma S) is non empty Element of bool (bool the carrier of (Sigma S))
bool the carrier of (Sigma S) is non empty set
bool (bool the carrier of (Sigma S)) is non empty set
TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) is non empty strict TopSpace-like TopStruct
[: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty strict TopSpace-like TopStruct
the topology of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty Element of bool (bool the carrier of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:])
the carrier of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
bool the carrier of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set
bool (bool the carrier of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:]) is non empty set
[:(Sigma N),(Sigma S):] is non empty strict TopSpace-like TopStruct
the topology of [:(Sigma N),(Sigma S):] is non empty Element of bool (bool the carrier of [:(Sigma N),(Sigma S):])
the carrier of [:(Sigma N),(Sigma S):] is non empty set
bool the carrier of [:(Sigma N),(Sigma S):] is non empty set
bool (bool the carrier of [:(Sigma N),(Sigma S):]) is non empty set
sigma [:N,S:] is non empty Element of bool (bool the carrier of [:N,S:])
Scott-Convergence [:N,S:] is Relation-like V246([:N,S:]) V247([:N,S:]) M36([:N,S:])
K403([:N,S:],(Scott-Convergence [:N,S:])) is non empty strict TopSpace-like TopStruct
the topology of K403([:N,S:],(Scott-Convergence [:N,S:])) is non empty Element of bool (bool the carrier of K403([:N,S:],(Scott-Convergence [:N,S:])))
the carrier of K403([:N,S:],(Scott-Convergence [:N,S:])) is non empty set
bool the carrier of K403([:N,S:],(Scott-Convergence [:N,S:])) is non empty set
bool (bool the carrier of K403([:N,S:],(Scott-Convergence [:N,S:]))) is non empty set
the carrier of [: the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] \/ the carrier of [: the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of N, the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:] is non empty set
C is non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of [:N,S:], the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of [:N,S:]
the topology of C is non empty Element of bool (bool the carrier of C)
the carrier of C is non empty set
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
[:N,S:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
sigma 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
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
InclPoset (sigma S) is non empty strict reflexive transitive antisymmetric non void RelStr
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,S:]
the carrier of T 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 T, the topology of T #) is non empty strict TopSpace-like TopStruct
y is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N
BC is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of S
[:y,BC:] is non empty strict TopSpace-like TopStruct
lambda [:N,S:] is non empty Element of bool (bool the carrier of [:N,S:])
the carrier of [:N,S:] is non empty set
bool the carrier of [:N,S:] is non empty set
bool (bool the carrier of [:N,S:]) is non empty set
the topology of [:y,BC:] is non empty Element of bool (bool the carrier of [:y,BC:])
the carrier of [:y,BC:] is non empty set
bool the carrier of [:y,BC:] is non empty set
bool (bool the carrier of [:y,BC:]) is non empty set
the carrier of y is non empty set
the InternalRel of y is non empty Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of BC is non empty set
the InternalRel of BC is non empty Relation-like the carrier of BC -defined the carrier of BC -valued Element of bool [: the carrier of BC, the carrier of BC:]
[: the carrier of BC, the carrier of BC:] is non empty set
bool [: the carrier of BC, the carrier of BC:] is non empty set
RelStr(# the carrier of BC, the InternalRel of BC #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of T is non empty 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 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of [:N,S:] is non empty Relation-like the carrier of [:N,S:] -defined the carrier of [:N,S:] -valued Element of bool [: the carrier of [:N,S:], the carrier of [:N,S:]:]
[: the carrier of [:N,S:], the carrier of [:N,S:]:] is non empty set
bool [: the carrier of [:N,S:], the carrier of [:N,S:]:] is non empty set
RelStr(# the carrier of [:N,S:], the InternalRel of [:N,S:] #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
[: the carrier of y, the carrier of S:] is non empty set
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
S is Element of the carrier of N
S "/\" is Relation-like the carrier of N -defined the carrier of N -valued Function-like V18( the carrier of N, the carrier of N) meet-preserving directed-sups-preserving Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
bool the carrier of N is non empty set
T is non empty Element of bool the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
S is Element of the carrier of N
S "/\" is Relation-like the carrier of N -defined the carrier of N -valued Function-like V18( the carrier of N, the carrier of N) meet-preserving directed-sups-preserving Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
[:N,N:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]
the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] is non empty set
the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:])
bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]) is non empty set
TopStruct(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] #) is non empty strict TopSpace-like TopStruct
[:N,N:] is non empty strict TopSpace-like TopStruct
the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] is non empty Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] -defined the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]:]
[: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of [:N,N:] is non empty set
the InternalRel of [:N,N:] is non empty Relation-like the carrier of [:N,N:] -defined the carrier of [:N,N:] -valued Element of bool [: the carrier of [:N,N:], the carrier of [:N,N:]:]
[: the carrier of [:N,N:], the carrier of [:N,N:]:] is non empty set
bool [: the carrier of [:N,N:], the carrier of [:N,N:]:] is non empty set
RelStr(# the carrier of [:N,N:], the InternalRel of [:N,N:] #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
[: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of N:] is non empty set
inf_op N is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) V144([:N,N:],N) infs-preserving meet-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of [:N,N:], the carrier of N:]
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
T is Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of N) Element of bool [: the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:], the carrier of N:]
y is Element of bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]
bool the carrier of [:N,N:] is non empty set
BC is non empty directed Element of bool the carrier of [:N,N:]
y is Element of bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of [:N,N:]
bool the carrier of [:N,N:] is non empty set
BC is Element of bool the carrier of [:N,N:]
the topology of N is non empty Element of bool (bool the carrier of N)
TopStruct(# the carrier of N, the topology of N #) is non empty strict TopSpace-like TopStruct
the carrier of [:N,N:] is non empty set
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
y is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) Element of bool [: the carrier of [:N,N:], the carrier of N:]
T is set
N is set
y is set
S is set
pr2 (N,S) is Relation-like [:N,S:] -defined S -valued Function-like V18([:N,S:],S) Element of bool [:[:N,S:],S:]
[:N,S:] is set
[:[:N,S:],S:] is set
bool [:[:N,S:],S:] is non empty set
pr1 (N,S) is Relation-like [:N,S:] -defined N -valued Function-like V18([:N,S:],N) Element of bool [:[:N,S:],N:]
[:[:N,S:],N:] is set
bool [:[:N,S:],N:] is non empty set
<:(pr2 (N,S)),(pr1 (N,S)):> is Relation-like Function-like one-to-one set
dom <:(pr2 (N,S)),(pr1 (N,S)):> is set
dom (pr2 (N,S)) is Relation-like N -defined S -valued Element of bool [:N,S:]
bool [:N,S:] is non empty set
dom (pr1 (N,S)) is Relation-like N -defined S -valued Element of bool [:N,S:]
(dom (pr2 (N,S))) /\ (dom (pr1 (N,S))) is Relation-like N -defined S -valued Element of bool [:N,S:]
(dom (pr2 (N,S))) /\ [:N,S:] is Relation-like N -defined S -valued Element of bool [:N,S:]
[:N,S:] /\ [:N,S:] is set
[T,y] is set
{T,y} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,y},{T}} is non empty finite V32() set
<:(pr2 (N,S)),(pr1 (N,S)):> . [T,y] is set
(pr2 (N,S)) . (T,y) is set
(pr2 (N,S)) . [T,y] is set
(pr1 (N,S)) . (T,y) is set
(pr1 (N,S)) . [T,y] is set
[((pr2 (N,S)) . (T,y)),((pr1 (N,S)) . (T,y))] is set
{((pr2 (N,S)) . (T,y)),((pr1 (N,S)) . (T,y))} is non empty finite set
{((pr2 (N,S)) . (T,y))} is non empty trivial finite 1 -element set
{{((pr2 (N,S)) . (T,y)),((pr1 (N,S)) . (T,y))},{((pr2 (N,S)) . (T,y))}} is non empty finite V32() set
[y,((pr1 (N,S)) . (T,y))] is set
{y,((pr1 (N,S)) . (T,y))} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,((pr1 (N,S)) . (T,y))},{y}} is non empty finite V32() set
[y,T] is set
{y,T} is non empty finite set
{{y,T},{y}} is non empty finite V32() set
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
[:N,N:] is non empty strict TopSpace-like TopStruct
the carrier of [:N,N:] is non empty set
bool the carrier of [:N,N:] is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
id the carrier of N is non empty Relation-like the carrier of N -defined the carrier of N -valued total Element of bool [: the carrier of N, the carrier of N:]
inf_op N is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) V144([:N,N:],N) infs-preserving meet-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of [:N,N:], the carrier of N:]
[:N,N:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of [:N,N:] is non empty set
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
pr1 ( the carrier of N, the carrier of N) is Relation-like [: the carrier of N, the carrier of N:] -defined the carrier of N -valued Function-like V18([: the carrier of N, the carrier of N:], the carrier of N) Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
<:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):> is Relation-like Function-like set
S is Element of bool the carrier of [:N,N:]
[: the carrier of [:N,N:], the carrier of [:N,N:]:] is non empty set
bool [: the carrier of [:N,N:], the carrier of [:N,N:]:] is non empty set
BC is Element of bool the carrier of [:N,N:]
BC is Relation-like the carrier of [:N,N:] -defined the carrier of [:N,N:] -valued Function-like V18( the carrier of [:N,N:], the carrier of [:N,N:]) Element of bool [: the carrier of [:N,N:], the carrier of [:N,N:]:]
A is Element of the carrier of N
C is Element of the carrier of N
[A,C] is Element of the carrier of [:N,N:]
{A,C} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,C},{A}} is non empty finite V32() set
BC . [A,C] is set
A "/\" C is Element of the carrier of N
[A,(A "/\" C)] is Element of the carrier of [:N,N:]
{A,(A "/\" C)} is non empty finite set
{{A,(A "/\" C)},{A}} is non empty finite V32() set
dom (pr1 ( the carrier of N, the carrier of N)) is Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
dom (inf_op N) is Element of bool the carrier of [:N,N:]
bool the carrier of [:N,N:] is non empty set
(pr1 ( the carrier of N, the carrier of N)) . (A,C) is Element of the carrier of N
[A,C] is set
(pr1 ( the carrier of N, the carrier of N)) . [A,C] is set
(inf_op N) . (A,C) is set
(inf_op N) . [A,C] is set
[((pr1 ( the carrier of N, the carrier of N)) . (A,C)),((inf_op N) . (A,C))] is set
{((pr1 ( the carrier of N, the carrier of N)) . (A,C)),((inf_op N) . (A,C))} is non empty finite set
{((pr1 ( the carrier of N, the carrier of N)) . (A,C))} is non empty trivial finite 1 -element set
{{((pr1 ( the carrier of N, the carrier of N)) . (A,C)),((inf_op N) . (A,C))},{((pr1 ( the carrier of N, the carrier of N)) . (A,C))}} is non empty finite V32() set
[A,((inf_op N) . (A,C))] is set
{A,((inf_op N) . (A,C))} is non empty finite set
{{A,((inf_op N) . (A,C))},{A}} is non empty finite V32() set
BC " S is Element of bool the carrier of [:N,N:]
A is set
C is set
c₉ is set
[C,c₉] is set
{C,c₉} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,c₉},{C}} is non empty finite V32() set
K is Element of the carrier of N
KK is Element of the carrier of N
K "/\" KK is Element of the carrier of N
[K,KK] is Element of the carrier of [:N,N:]
{K,KK} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,KK},{K}} is non empty finite V32() set
BC . [K,KK] is set
[K,K] is Element of the carrier of [:N,N:]
{K,K} is non empty finite set
{{K,K},{K}} is non empty finite V32() set
BC . A is set
dom BC is Element of bool the carrier of [:N,N:]
A is set
BC . A is set
C is set
c₉ is set
[C,c₉] is set
{C,c₉} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,c₉},{C}} is non empty finite V32() set
K is Element of the carrier of N
KK is Element of the carrier of N
K "/\" KK is Element of the carrier of N
[K,(K "/\" KK)] is Element of the carrier of [:N,N:]
{K,(K "/\" KK)} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,(K "/\" KK)},{K}} is non empty finite V32() set
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
A is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) Element of bool [: the carrier of [:N,N:], the carrier of N:]
N ~ is non empty strict reflexive transitive antisymmetric non void RelStr
the InternalRel of N ~ is Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
RelStr(# the carrier of N,( the InternalRel of N ~) #) is strict RelStr
the carrier of (N ~) is non empty set
[: the carrier of (N ~), the carrier of (N ~):] is non empty set
the InternalRel of (N ~) is non empty Relation-like the carrier of (N ~) -defined the carrier of (N ~) -valued Element of bool [: the carrier of (N ~), the carrier of (N ~):]
bool [: the carrier of (N ~), the carrier of (N ~):] is non empty set
the InternalRel of N /\ the InternalRel of (N ~) is Relation-like the carrier of N -defined the carrier of (N ~) -defined the carrier of N -valued the carrier of (N ~) -valued Element of bool [: the carrier of (N ~), the carrier of (N ~):]
pr2 ( the carrier of N, the carrier of N) is Relation-like [: the carrier of N, the carrier of N:] -defined the carrier of N -valued Function-like V18([: the carrier of N, the carrier of N:], the carrier of N) Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
<:(pr2 ( the carrier of N, the carrier of N)),(pr1 ( the carrier of N, the carrier of N)):> is Relation-like [: the carrier of N, the carrier of N:] -defined [: the carrier of N, the carrier of N:] -valued Function-like one-to-one V18([: the carrier of N, the carrier of N:],[: the carrier of N, the carrier of N:]) Element of bool [:[: the carrier of N, the carrier of N:],[: the carrier of N, the carrier of N:]:]
[:[: the carrier of N, the carrier of N:],[: the carrier of N, the carrier of N:]:] is non empty set
bool [:[: the carrier of N, the carrier of N:],[: the carrier of N, the carrier of N:]:] is non empty set
BC is Element of bool the carrier of [:N,N:]
T is Element of bool the carrier of [:N,N:]
y is Element of bool the carrier of [:N,N:]
BC is Element of bool the carrier of [:N,N:]
S is Relation-like the carrier of [:N,N:] -defined the carrier of [:N,N:] -valued Function-like V18( the carrier of [:N,N:], the carrier of [:N,N:]) continuous Element of bool [: the carrier of [:N,N:], the carrier of [:N,N:]:]
dom S is Element of bool the carrier of [:N,N:]
S .: BC is Element of bool the carrier of [:N,N:]
A is Element of bool the carrier of [:N,N:]
C is set
c₉ is set
S . c₉ is set
K is set
KK is set
[K,KK] is set
{K,KK} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,KK},{K}} is non empty finite V32() set
[KK,K] is set
{KK,K} is non empty finite set
{KK} is non empty trivial finite 1 -element set
{{KK,K},{KK}} is non empty finite V32() set
C is set
c₉ is set
K is set
[c₉,K] is set
{c₉,K} is non empty finite set
{c₉} is non empty trivial finite 1 -element set
{{c₉,K},{c₉}} is non empty finite V32() set
[K,c₉] is set
{K,c₉} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,c₉},{K}} is non empty finite V32() set
S . [K,c₉] is set
N is non empty reflexive non void RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
{ b₁ where b₁ is Element of the carrier of N : S₁[b₁] } is set
N is non empty reflexive antisymmetric non void RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is empty proper V23() V27() finite V32() cardinal {} -element directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N
(N,S) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
T is set
y is Element of the carrier of N
{y} is non empty trivial finite 1 -element Element of bool the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
N is non empty reflexive non void RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of bool the carrier of N
T is Element of bool the carrier of N
(N,S) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
(N,T) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not T misses b₂ ) } is set
y is set
BC is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
N is non empty reflexive non void RelStr
the carrier of N is non empty set
S is Element of the carrier of N
uparrow S is non empty filtered Element of bool the carrier of N
bool the carrier of N is non empty set
{S} is non empty trivial finite 1 -element Element of bool the carrier of N
uparrow {S} is non empty Element of bool the carrier of N
(N,(uparrow S)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow S misses b₂ ) } is set
wayabove S is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : S is_way_below b₁ } is set
T is set
y is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
(uparrow S) /\ BC is Element of bool the carrier of N
BC is set
A is Element of the carrier of N
T is set
y is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
BC is Element of the carrier of N
N is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima Scott non void TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is upper Element of bool the carrier of N
Int S is open Element of bool the carrier of N
(N,S) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
T is set
y is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
N is non empty reflexive non void RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of bool the carrier of N
(N,S) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
T is Element of bool the carrier of N
(N,T) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not T misses b₂ ) } is set
(N,S) \/ (N,T) is Element of bool the carrier of N
S \/ T is Element of bool the carrier of N
(N,(S \/ T)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S \/ T misses b₂ ) } is set
y is set
BC is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
A is Element of the carrier of N
S /\ BC is Element of bool the carrier of N
T /\ BC is Element of bool the carrier of N
(S /\ BC) \/ (T /\ BC) is Element of bool the carrier of N
(S \/ T) /\ BC is Element of bool the carrier of N
A is Element of the carrier of N
T /\ BC is Element of bool the carrier of N
S /\ BC is Element of bool the carrier of N
(S /\ BC) \/ (T /\ BC) is Element of bool the carrier of N
(S \/ T) /\ BC is Element of bool the carrier of N
(S \/ T) /\ BC is Element of bool the carrier of N
(S \/ T) /\ BC is Element of bool the carrier of N
N is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void satisfying_MC meet-continuous RelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is upper Element of bool the carrier of N
(N,S) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S misses b₂ ) } is set
T is upper Element of bool the carrier of N
(N,T) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not T misses b₂ ) } is set
(N,S) \/ (N,T) is Element of bool the carrier of N
S \/ T is Element of bool the carrier of N
(N,(S \/ T)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not S \/ T misses b₂ ) } is set
y is set
BC is Element of the carrier of N
BC is non empty directed Element of bool the carrier of N
"\/" (BC,N) is Element of the carrier of N
A is non empty directed Element of bool the carrier of N
"\/" (A,N) is Element of the carrier of N
BC "/\" BC is Element of the carrier of N
("\/" (BC,N)) "/\" ("\/" (A,N)) is Element of the carrier of N
BC "/\" A is non empty directed Element of bool the carrier of N
"\/" ((BC "/\" A),N) is Element of the carrier of N
C is Element of the carrier of N
(S \/ T) /\ (BC "/\" A) is Element of bool the carrier of N
S /\ (BC "/\" A) is Element of bool the carrier of N
T /\ (BC "/\" A) is Element of bool the carrier of N
(S /\ (BC "/\" A)) \/ (T /\ (BC "/\" A)) is Element of bool the carrier of N
N is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima Scott non void satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is finite Element of bool the carrier of N
uparrow S is upper Element of bool the carrier of N
Int (uparrow S) is open Element of bool the carrier of N
{ (wayabove b₁) where b₁ is Element of the carrier of N : b₁ in S } is set
union { (wayabove b₁) where b₁ is Element of the carrier of N : b₁ in S } is set
bool (bool the carrier of N) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of N : b₁ in a₁ } is set
{ (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in a₁ } is set
union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in a₁ } is set
T is set
y is set
{ (uparrow b₁) where b₁ is Element of the carrier of N : b₁ in y } is set
{ (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in y } is set
union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in y } is set
{T} is non empty trivial finite 1 -element set
y \/ {T} is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of N : b₁ in y \/ {T} } is set
{ (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in y \/ {T} } is set
union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in y \/ {T} } is set
BC is Element of the carrier of N
uparrow BC is non empty filtered upper Element of bool the carrier of N
{BC} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {BC} is non empty upper Element of bool the carrier of N
(N,(uparrow BC)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow BC misses b₂ ) } is set
(union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in y } ) \/ (N,(uparrow BC)) is set
BC is set
A is Element of the carrier of N
uparrow A is non empty filtered upper Element of bool the carrier of N
{A} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {A} is non empty upper Element of bool the carrier of N
(N,(uparrow A)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow A misses b₂ ) } is set
BC is set
A is set
C is Element of the carrier of N
uparrow C is non empty filtered upper Element of bool the carrier of N
{C} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {C} is non empty upper Element of bool the carrier of N
(N,(uparrow C)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow C misses b₂ ) } is set
BC is Element of bool (bool the carrier of N)
union BC is Element of bool the carrier of N
(N,(union BC)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not union BC misses b₂ ) } is set
BC is Element of bool (bool the carrier of N)
union BC is Element of bool the carrier of N
(N,(union BC)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not union BC misses b₂ ) } is set
{(uparrow BC)} is non empty trivial finite 1 -element Element of bool (bool the carrier of N)
BC \/ {(uparrow BC)} is non empty Element of bool (bool the carrier of N)
A is Element of bool (bool the carrier of N)
union A is Element of bool the carrier of N
(N,(union A)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not union A misses b₂ ) } is set
C is set
c₉ is Element of the carrier of N
uparrow c₉ is non empty filtered upper Element of bool the carrier of N
{c₉} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {c₉} is non empty upper Element of bool the carrier of N
C is set
c₉ is Element of the carrier of N
uparrow c₉ is non empty filtered upper Element of bool the carrier of N
{c₉} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {c₉} is non empty upper Element of bool the carrier of N
{(uparrow c₉)} is non empty trivial finite 1 -element Element of bool (bool the carrier of N)
(union BC) \/ (uparrow BC) is non empty Element of bool the carrier of N
C is set
c₉ is set
C is set
c₉ is set
C is Element of bool the carrier of N
c₉ is Element of the carrier of N
uparrow c₉ is non empty filtered upper Element of bool the carrier of N
{c₉} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {c₉} is non empty upper Element of bool the carrier of N
{ (uparrow b₁) where b₁ is Element of the carrier of N : b₁ in {} } is set
{ (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in {} } is set
union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in {} } is set
T is Element of bool (bool the carrier of N)
union T is Element of bool the carrier of N
(N,(union T)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not union T misses b₂ ) } is set
y is empty proper V23() V27() finite V32() cardinal {} -element open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N
(N,y) is empty proper V23() V27() finite V32() cardinal {} -element open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not y misses b₂ ) } is set
{ H₂(b₁) where b₁ is Element of the carrier of N : b₁ in {} } is set
{ H₁(b₁) where b₁ is Element of the carrier of N : b₁ in {} } is set
{ (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in S } is set
T is set
y is Element of the carrier of N
uparrow y is non empty filtered upper Element of bool the carrier of N
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {y} is non empty upper Element of bool the carrier of N
(N,(uparrow y)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow y misses b₂ ) } is set
wayabove y is upper Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : y is_way_below b₁ } is set
T is set
y is Element of the carrier of N
wayabove y is upper Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : y is_way_below b₁ } is set
uparrow y is non empty filtered upper Element of bool the carrier of N
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of N
uparrow {y} is non empty upper Element of bool the carrier of N
(N,(uparrow y)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow y misses b₂ ) } is set
{ (uparrow b₁) where b₁ is Element of the carrier of N : b₁ in S } is set
union { (N,(uparrow b₁)) where b₁ is Element of the carrier of N : b₁ in S } is set
(N,(uparrow S)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not uparrow S misses b₂ ) } is set
T is Element of bool (bool the carrier of N)
union T is Element of bool the carrier of N
(N,(union T)) is Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : for b₂ being non empty directed Element of bool the carrier of N holds
( not b₁ <= "\/" (b₂,N) or not union T misses b₂ ) } is set
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
the carrier of N is non empty set
S is Element of the carrier of N
waybelow S is non empty directed lower property(S) Element of bool the carrier of N
bool the carrier of N is non empty set
{ b₁ where b₁ is Element of the carrier of N : b₁ is_way_below S } is set
T is Element of the carrier of N
waybelow T is non empty directed lower property(S) Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : b₁ is_way_below T } is set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
{ (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of bool the carrier of N : ( b₁ in sigma N & b₂ is finite ) } is set
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
y is non empty reflexive transitive antisymmetric with_infima non void RelStr
the carrier of y is non empty set
BC is Element of the carrier of y
BC is Element of the carrier of y
BC "/\" BC is Element of the carrier of y
A is Element of the carrier of y
A "/\" A is Element of the carrier of y
y is Element of the carrier of N
BC is Element of the carrier of N
y "/\" BC is Element of the carrier of N
BC is Element of bool the carrier of N
A is Element of bool the carrier of N
S is non empty open quasi_basis Element of bool (bool the carrier of N)
{ b₁ where b₁ is Element of bool the carrier of N : ( b₁ in S & b₁ c= A ) } is set
union { b₁ where b₁ is Element of bool the carrier of N : ( b₁ in S & b₁ c= A ) } is set
C is set
c₉ is Element of bool the carrier of N
K is Element of bool the carrier of N
KK is Element of bool the carrier of N
uparrow KK is upper Element of bool the carrier of N
K \ (uparrow KK) is Element of bool the carrier of N
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
c₁₂ is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
b is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{c₁₂,b} is non empty finite Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
BC /\ K is Element of bool the carrier of N
V is Element of bool the carrier of N
U1 is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
uparrow U1 is upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
uparrow V is upper Element of bool the carrier of N
sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is Relation-like V246( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) V247( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) M36( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)))
the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N))) is non empty set
z is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
V \ (uparrow KK) is Element of bool the carrier of N
z \ (uparrow KK) is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
U2 is set
c₁₂ "/\" b is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{y,BC} is non empty finite closed Element of bool the carrier of N
"/\" ({y,BC},N) is Element of the carrier of N
"/\" ({c₁₂,b}, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
U2 is finite Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
uparrow U2 is upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
Int (uparrow U2) is open Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{ (wayabove b₁) where b₁ is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : b₁ in U2 } is set
union { (wayabove b₁) where b₁ is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : b₁ in U2 } is set
U2 is set
IT is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
wayabove IT is upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{ b₁ where b₁ is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : IT is_way_below b₁ } is set
U2 is Element of the carrier of N
wayabove U2 is upper Element of bool the carrier of N
{ b₁ where b₁ is Element of the carrier of N : U2 is_way_below b₁ } is set
F is Element of the carrier of N
uparrow F is non empty filtered upper Element of bool the carrier of N
{F} is non empty trivial finite 1 -element closed compact Element of bool the carrier of N
uparrow {F} is non empty upper Element of bool the carrier of N
F is Element of the carrier of N
F is Element of the carrier of N
N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void TopRelStr
N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void TopRelStr
N is non empty TopSpace-like TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
S is Element of the carrier of N
T is non empty open S -quasi_basis Element of bool (bool the carrier of N)
y is non empty basis of S
BC is Element of bool the carrier of N
subrelstr BC is strict V156(N) SubRelStr of N
N is non empty TopSpace-like TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of the carrier of N
T is non empty basis of S
y is Element of bool the carrier of N
subrelstr y is strict V156(N) SubRelStr of N
N is non empty TopRelStr
S is non empty anti-discrete TopRelStr
the carrier of S is non empty set
{ the carrier of S} is non empty trivial finite 1 -element set
bool the carrier of S is non empty set
[#] S is non empty non proper dense lower upper Element of bool the carrier of S
subrelstr ([#] S) is non empty strict V156(S) meet-inheriting join-inheriting infs-inheriting sups-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of S
y is Element of bool the carrier of S
subrelstr y is strict V156(S) SubRelStr of S
BC is meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of N
y is Element of the carrier of S
bool (bool the carrier of S) is non empty set
BC is open y -quasi_basis Element of bool (bool the carrier of S)
BC is Element of bool the carrier of S
subrelstr BC is strict V156(S) SubRelStr of S
y is Element of the carrier of S
BC is basis of y
BC is Element of bool the carrier of S
subrelstr BC is strict V156(S) SubRelStr of S
N is non empty trivial finite 1 -element TopRelStr
S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () TopRelStr
the carrier of S is non empty trivial finite 1 -element set
T is Element of the carrier of S
bool the carrier of S is non empty finite V32() set
{ the carrier of S} is non empty trivial finite V32() 1 -element set
y is non empty finite V32() basis of T
BC is trivial finite closed directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of S
subrelstr BC is strict reflexive transitive antisymmetric V156(S) directed SubRelStr of S
[#] S is non empty trivial non proper finite 1 -element open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of S
subrelstr ([#] S) is non empty strict reflexive transitive antisymmetric V156(S) meet-inheriting join-inheriting infs-inheriting sups-inheriting filtered-infs-inheriting directed-sups-inheriting directed with_suprema with_infima non void SubRelStr of S
BC is meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of N
the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () () TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () () TopRelStr
N is non empty TopSpace-like reflexive transitive antisymmetric with_infima topological_semilattice non void TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
S is Element of bool the carrier of N
subrelstr S is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
Cl S is closed Element of bool the carrier of N
subrelstr (Cl S) is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
BC is Element of the carrier of N
the carrier of (subrelstr (Cl S)) is set
BC is Element of the carrier of N
{BC,BC} is non empty finite Element of bool the carrier of N
"/\" ({BC,BC},N) is Element of the carrier of N
BC "/\" BC is Element of the carrier of N
[:N,N:] is non empty strict TopSpace-like TopStruct
C is a_neighborhood of BC "/\" BC
the carrier of [:N,N:] is non empty set
[: the carrier of N, the carrier of N:] is non empty set
[BC,BC] is Element of the carrier of [:N,N:]
[:N,N:] is non empty strict reflexive transitive antisymmetric with_infima non void RelStr
the carrier of [:N,N:] is non empty set
{BC,BC} is non empty finite set
{BC} is non empty trivial finite 1 -element set
{{BC,BC},{BC}} is non empty finite V32() set
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
inf_op N is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) V144([:N,N:],N) Element of bool [: the carrier of [:N,N:], the carrier of N:]
[: the carrier of [:N,N:], the carrier of N:] is non empty set
bool [: the carrier of [:N,N:], the carrier of N:] is non empty set
K is Relation-like the carrier of [:N,N:] -defined the carrier of N -valued Function-like V18( the carrier of [:N,N:], the carrier of N) Element of bool [: the carrier of [:N,N:], the carrier of N:]
c₉ is Element of the carrier of [:N,N:]
K . c₉ is set
K . (BC,BC) is set
[BC,BC] is set
K . [BC,BC] is set
KK is a_neighborhood of c₉
K .: KK is Element of bool the carrier of N
bool the carrier of [:N,N:] is non empty set
bool (bool the carrier of [:N,N:]) is non empty set
Int KK is open Element of bool the carrier of [:N,N:]
c₁₂ is Element of bool (bool the carrier of [:N,N:])
union c₁₂ is Element of bool the carrier of [:N,N:]
b is set
z is Element of bool the carrier of N
V is Element of bool the carrier of N
[:z,V:] is Element of bool the carrier of [:N,N:]
bool the carrier of [:N,N:] is non empty set
Int z is open Element of bool the carrier of N
Int V is open Element of bool the carrier of N
U1 is a_neighborhood of BC
U2 is set
U2 is a_neighborhood of BC
IT is set
U2 is Element of the carrier of N
F is Element of the carrier of N
[U2,F] is Element of the carrier of [:N,N:]
{U2,F} is non empty finite set
{U2} is non empty trivial finite 1 -element set
{{U2,F},{U2}} is non empty finite V32() set
U2 "/\" F is Element of the carrier of N
dom K is Element of bool the carrier of [:N,N:]
K . (U2,F) is set
[U2,F] is set
K . [U2,F] is set
IT is Element of the carrier of N
{U2,F} is non empty finite Element of bool the carrier of N
the carrier of (subrelstr S) is set
"/\" ({U2,F},N) is Element of the carrier of N
IT is Element of the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
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 carrier of N is non empty set
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
T is Element of the carrier of N
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
y is Element of bool (bool the carrier of N)
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
{ (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of bool the carrier of N : ( b₁ in sigma N & b₂ is finite ) } is set
BC is non empty open quasi_basis Element of bool (bool the carrier of N)
the topology of N is non empty Element of bool (bool the carrier of N)
C is Element of bool the carrier of N
A is Element of the carrier of S
c₉ is non empty open A -quasi_basis Element of bool (bool the carrier of S)
{ b₁ where b₁ is Element of bool the carrier of N : ( b₁ in BC & b₁ c= C ) } is set
union { b₁ where b₁ is Element of bool the carrier of N : ( b₁ in BC & b₁ c= C ) } is set
K is set
KK is Element of bool the carrier of N
c₁₂ is Element of bool the carrier of N
b is Element of bool the carrier of N
uparrow b is upper Element of bool the carrier of N
c₁₂ \ (uparrow b) is Element of bool the carrier of N
z is finite closed Element of bool the carrier of N
uparrow z is upper Element of bool the carrier of N
V is Element of bool the carrier of S
sigma S is non empty Element of bool (bool the carrier of S)
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
U1 is Element of bool the carrier of S
U2 is Element of bool the carrier of N
U2 is non empty filtered upper Element of bool the carrier of N
U2 \ (uparrow z) is Element of bool the carrier of N
U1 \ (uparrow z) is Element of bool the carrier of S
IT is Element of bool the carrier of N
IT is Element of bool the carrier of N
U2 is non empty filtered upper Element of bool the carrier of N
F is finite closed Element of bool the carrier of N
uparrow F is upper Element of bool the carrier of N
U2 \ (uparrow F) is Element of bool the carrier of N
BC is Element of bool (bool the carrier of N)
BC is Element of bool the carrier of N
A is Element of bool the carrier of N
K is Element of bool the carrier of N
C is non empty filtered upper Element of bool the carrier of N
c₉ is finite closed Element of bool the carrier of N
uparrow c₉ is upper Element of bool the carrier of N
C \ (uparrow c₉) is Element of bool the carrier of N
BC is set
A is Element of bool the carrier of N
K is Element of bool the carrier of N
C is non empty filtered upper Element of bool the carrier of N
c₉ is finite closed Element of bool the carrier of N
uparrow c₉ is upper Element of bool the carrier of N
C \ (uparrow c₉) is Element of bool the carrier of N
Intersect BC is Element of bool the carrier of N
BC is Element of bool the carrier of N
c₉ is Element of bool the carrier of N
A is non empty filtered upper Element of bool the carrier of N
C is finite closed Element of bool the carrier of N
uparrow C is upper Element of bool the carrier of N
A \ (uparrow C) is Element of bool the carrier of N
BC is non empty open T -quasi_basis Element of bool (bool the carrier of N)
A is Element of bool the carrier of N
subrelstr A is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
K is Element of bool the carrier of N
C is non empty filtered upper Element of bool the carrier of N
c₉ is finite closed Element of bool the carrier of N
uparrow c₉ is upper Element of bool the carrier of N
C \ (uparrow c₉) is Element of bool the carrier of N
c₁₂ is Element of the carrier of N
the carrier of (subrelstr A) is set
b is Element of the carrier of N
{c₁₂,b} is non empty finite closed Element of bool the carrier of N
"/\" ({c₁₂,b},N) is Element of the carrier of N
c₁₂ "/\" b is Element of the carrier of N
z is Element of the carrier of N
z is Element of the carrier of N
z "/\" z is Element of the carrier of N
T is Element of the carrier of S
y is Element of the carrier of N
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
BC is non empty open y -quasi_basis Element of bool (bool the carrier of N)
{ (uparrow b₁) where b₁ is Element of bool the carrier of N : b₁ in BC } is set
BC is non empty open T -quasi_basis Element of bool (bool the carrier of S)
A is Element of bool the carrier of S
C is Element of bool the carrier of N
uparrow C is upper Element of bool the carrier of N
subrelstr C is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
sigma S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
T is Element of the carrier of N
{ ("/\" (b₁,S)) where b₁ is Element of bool the carrier of S : ( T in b₁ & b₁ in sigma S ) } is set
{ ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } is set
BC is set
BC is Element of bool the carrier of S
"/\" (BC,S) is Element of the carrier of S
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
sigma N is non empty Element of bool (bool the carrier of N)
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
A is Element of bool the carrier of N
"/\" (A,N) is Element of the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of S is non empty set
bool the carrier of S is non empty set
sigma S is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)
K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct
the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))
the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool the carrier of K403(S,(Scott-Convergence S)) is non empty set
bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set
T is Element of the carrier of N
{ ("/\" (b₁,S)) where b₁ is Element of bool the carrier of S : ( T in b₁ & b₁ in sigma S ) } is set
{ ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } is set
BC is set
A is Element of bool the carrier of N
"/\" (A,N) is Element of the carrier of N
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of S is non empty 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 non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
C is Element of bool the carrier of S
uparrow C is upper Element of bool the carrier of S
"/\" (C,S) is Element of the carrier of S
"/\" ((uparrow C),S) is Element of the carrier of S
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
T is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
y is non empty open T -quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
BC is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is Relation-like V246( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) V247( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) M36( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)))
the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N))) is non empty set
InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
T is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
y is Element of the carrier of N
BC is non empty open y -quasi_basis Element of bool (bool the carrier of N)
{ (uparrow b₁) where b₁ is Element of bool the carrier of N : b₁ in BC } is set
BC is non empty open T -quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
A is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
C is Element of bool the carrier of N
uparrow C is upper Element of bool the carrier of N
subrelstr C is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
T is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } , the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr
N is non empty TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) V248(N) V249(N) V250(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
N is non empty TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) V248(N) V249(N) V250(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous RelStr
N is non empty TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson topological_semilattice locally-compact non void compact () () TopRelStr
the carrier of N is non empty set
S is Element of the carrier of N
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
T is non empty open S -quasi_basis Element of bool (bool the carrier of N)
{ (Cl b₁) where b₁ is Element of bool the carrier of N : b₁ in T } is set
bool the carrier of N is non empty Element of bool (bool the carrier of N)
BC is set
BC is Element of bool the carrier of N
Cl BC is closed Element of bool the carrier of N
BC is Element of bool (bool the carrier of N)
BC is a_neighborhood of S
Int BC is open Element of bool the carrier of N
A is Element of bool the carrier of N
Int A is open Element of bool the carrier of N
[#] N is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of N
{S} is non empty trivial finite 1 -element closed compact Element of bool the carrier of N
c₉ is Element of bool the carrier of N
Cl c₉ is closed Element of bool the carrier of N
K is Element of bool the carrier of N
Int K is open Element of bool the carrier of N
Cl K is closed Element of bool the carrier of N
Int (Cl K) is open Element of bool the carrier of N
KK is a_neighborhood of S
[#] N is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of N
C is a_neighborhood of S
Cl ([#] N) is closed Element of bool the carrier of N
[#] N is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of N
BC is non empty basis of S
A is Element of bool the carrier of N
subrelstr A is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
C is Element of bool the carrier of N
Cl C is closed Element of bool the carrier of N
subrelstr C is strict reflexive transitive antisymmetric V156(N) SubRelStr of N
N is non empty TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
S is Element of the carrier of N
{ ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( S in b₁ & b₁ in lambda N ) } is set
"\/" ( { ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( S in b₁ & b₁ in lambda N ) } ,N) is Element of the carrier of N
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N
sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is non empty set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) is non empty set
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is Relation-like V246( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) V247( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) V248( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) V249( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) V250( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) M36( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)
K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)))
the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) is non empty set
bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N))) is non empty set
InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
BC is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N
y is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N : ( y in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N ) } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N : ( y in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N ) } , the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N : ( S in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N ) } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N : ( S in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopAugmentation of N ) } ,N) is Element of the carrier of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
the carrier of N is non empty set
bool the carrier of N is non empty set
lambda N is non empty Element of bool (bool the carrier of N)
bool (bool the carrier of N) is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
T is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is Relation-like V246( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) V247( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) M36( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)))
the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N))) is non empty set
InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
T is Element of the carrier of N
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } , the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } ,N) is Element of the carrier of N
{ ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } is set
"\/" ( { ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } ,N) is Element of the carrier of N
T is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
{ ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } is set
"\/" ( { ("/\" (b₁,N)) where b₁ is Element of bool the carrier of N : ( T in b₁ & b₁ in lambda N ) } ,N) is Element of the carrier of N
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } ,N) is Element of the carrier of N
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : ( T in b₁ & b₁ in sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N ) } , the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]
[: the carrier of N, the carrier of N:] is non empty set
bool [: the carrier of N, the carrier of N:] is non empty set
RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_K algebraic satisfying_axiom_of_approximation continuous non void RelStr
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
CompactSublatt the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty strict reflexive transitive antisymmetric V156( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) join-inheriting with_suprema non void SubRelStr of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of (CompactSublatt the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N : b₁ in the carrier of (CompactSublatt the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) } is set
sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N is Relation-like V246( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) V247( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) M36( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty strict TopSpace-like TopStruct
the topology of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty Element of bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)))
the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
bool (bool the carrier of K403( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N))) is non empty set
InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr
y is non empty open quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
T is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_K algebraic satisfying_axiom_of_approximation continuous non void RelStr
y is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N
the carrier of (InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty non trivial set
bool the carrier of (InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)) is non empty set
y is Element of the carrier of (InclPoset (sigma the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N))
y is non empty open quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N)
N is non empty TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_K algebraic Lawson satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous () () TopRelStr
sigma N is non empty Element of bool (bool the carrier of N)
the carrier of N is non empty set
bool the carrier of N is non empty set
bool (bool the carrier of N) is non empty set
Scott-Convergence N is Relation-like V246(N) V247(N) V248(N) V249(N) V250(N) M36(N)
K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct
the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))
the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool the carrier of K403(N,(Scott-Convergence N)) is non empty set
bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set
InclPoset (sigma N) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous RelStr