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 /\ b1) where b1 is Element of S : verum } is set
union { (N /\ b1) where b1 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
{ b1 where b1 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))
c9 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
{ b1 where b1 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
{ b1 where b1 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
{ b1 where b1 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
{ b1 where b1 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
{ b1 where b1 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 /\ b1) where b1 is Element of S : verum } is set
union { (T /\ b1) where b1 is Element of S : verum } is set
{ (T "/\" b1) where b1 is Element of the carrier of (InclPoset (Ids N)) : b1 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))
c9 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
c9 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
{ b1 where b1 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 /\ b1) where b1 is Element of y : verum } is set
union { (T /\ b1) where b1 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
{ (b1 \ (uparrow b2)) where b1, b2 is Element of bool the carrier of N : ( b1 in sigma N & b2 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)
{ (b1 \ (uparrow b2)) where b1, b2 is Element of bool the carrier of N : ( b1 in sigma N & b2 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
F1() is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima Scott non void TopRelStr
the carrier of F1() is non empty set
{ F3(b1) where b1 is Element of the carrier of F1() : b1 in {} } is set
N is set
S is Element of the carrier of F1()
F3(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 "/\" b1) where b1 is Element of the carrier of N : b1 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 b1) where b1 is Element of bool the carrier of N : b1 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
c9 is Element of bool the carrier of N
uparrow c9 is upper Element of bool the carrier of N
C is Element of bool (bool the carrier of S)
c9 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)
c9 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
c9 is Element of bool the carrier of S
uparrow c9 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
c12 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
c9 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