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

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()
is set
bool 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 /\ () 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

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

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

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

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

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))

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

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

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

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 /\ () 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

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

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

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(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

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

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

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 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 [::]
[::] is non empty set
bool [::] 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 [::]
[::] is non empty set
bool [::] 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 is non empty Element of bool ()

bool () 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 () 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(N,)) is non empty set
() \/ () 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(S,)) is non empty set
() \/ () 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 () 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

the carrier of N is non empty set
bool the carrier of N is non empty set

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) \ 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) \ T is Element of bool the carrier of N

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 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 () is non empty set

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(N,)) is non empty set

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(N,)) is non empty set

lambda N is non empty Element of bool (bool the carrier 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 () is non empty set

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

K403(N,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(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

S \ (uparrow ({} N)) is Element of bool S
bool S is non empty set

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)

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(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)

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 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(S,)) is non empty set
omega S is Element of bool (bool the carrier of S)
() \/ () is non empty Element of bool (bool the carrier of S)
FinMeetCl (() \/ ()) is Element of bool (bool the carrier of S)
UniCl (FinMeetCl (() \/ ())) 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(N,)) is non empty set
omega N is Element of bool (bool the carrier of N)
() \/ () is non empty Element of bool (bool the carrier of N)
FinMeetCl (() \/ ()) is Element of bool (bool the carrier of N)
UniCl (FinMeetCl (() \/ ())) 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
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)

the carrier of S is non empty trivial finite 1 -element set
bool the carrier of S is non empty finite V32() 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

[::] is non empty finite set
bool [::] is non empty finite V32() set

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

bool () 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(N,)) is non empty set
omega N is Element of bool (bool the carrier of N)
() \/ () is non empty Element of bool (bool the carrier of N)
FinMeetCl (() \/ ()) is Element of bool (bool the carrier of N)
UniCl (FinMeetCl (() \/ ())) is Element of bool (bool the carrier of N)
() \/ () is non empty Element of bool (bool the carrier of N)
FinMeetCl (() \/ ()) is Element of bool (bool the carrier of N)

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

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

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

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

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(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)

the carrier of N is non empty set
bool the carrier of N is non empty set

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(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

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 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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(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,) is non empty strict TopSpace-like TopStruct
the topology of K403(N,) is non empty Element of bool (bool the carrier of K403(N,))
the carrier of K403(N,) is non empty set
bool the carrier of K403(N,) is non empty set
bool (bool the carrier of K403(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

the carrier of N is non empty set
bool the carrier of N is non empty set

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

the carrier of N is non empty set
bool the carrier of N is non empty set

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

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

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,) is non empty strict TopSpace-like TopStruct
the topology of K403(S,) is non empty Element of bool (bool the carrier of K403(S,))
the carrier of K403(S,) is non empty set
bool the carrier of K403(S,) is non empty set
bool (bool the carrier of K403(S,)) is non empty set

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,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 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 () 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 [::]
[::] is non empty set
bool [: