:: WAYBEL30 semantic presentation

K149() is non trivial V23() non finite cardinal limit_cardinal Element of bool K145()

K145() is set

bool K145() is non empty set

K87() is non trivial V23() non finite cardinal limit_cardinal set

bool K87() is non empty non trivial non finite set

{} is empty V23() V27() finite V32() cardinal {} -element set

the empty V23() V27() finite V32() cardinal {} -element set is empty V23() V27() finite V32() cardinal {} -element set

1 is non empty set

{{},1} is non empty finite set

bool K149() is non empty non trivial non finite set

K462() is non empty strict TopSpace-like TopStruct

the carrier of K462() is non empty set

K510() is set

{{}} is non empty trivial finite V32() 1 -element set

K467({{}}) is M44({{}})

[:K467({{}}),{{}}:] is set

bool [:K467({{}}),{{}}:] is non empty set

PFuncs (K467({{}}),{{}}) is set

K559() is strict TopStruct

N is set

S is non empty set

union S is set

N /\ (union S) is set

{ (N /\ b

union { (N /\ b

T is set

y is set

N /\ y is set

T is set

y is set

BC is Element of S

N /\ BC is set

N is non empty reflexive transitive non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

S is non empty directed Element of bool the carrier of (InclPoset (Ids N))

union S is set

the Element of S is Element of S

bool the carrier of N is non empty Element of bool (bool the carrier of N)

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

y is set

BC is non empty directed lower Element of bool the carrier of N

y is non empty directed lower Element of bool the carrier of N

BC is Element of bool the carrier of N

BC is non empty directed lower Element of bool the carrier of N

BC is Element of bool the carrier of N

BC is Element of bool the carrier of N

BC \/ BC is Element of bool the carrier of N

A is Element of the carrier of (InclPoset (Ids N))

C is Element of the carrier of (InclPoset (Ids N))

c

KK is non empty directed lower Element of bool the carrier of N

K is Element of bool the carrier of N

BC is Element of bool the carrier of N

BC is non empty directed lower Element of bool the carrier of N

the Element of y is Element of y

N is non empty reflexive transitive non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

T is Element of the carrier of (InclPoset (Ids N))

S is non empty directed Element of bool the carrier of (InclPoset (Ids N))

union S is set

y is Element of the carrier of (InclPoset (Ids N))

BC is set

N is non empty reflexive transitive non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

T is Element of the carrier of (InclPoset (Ids N))

S is non empty directed Element of bool the carrier of (InclPoset (Ids N))

union S is set

y is Element of the carrier of (InclPoset (Ids N))

BC is set

BC is set

A is Element of the carrier of (InclPoset (Ids N))

N is non empty reflexive transitive non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

T is non empty directed Element of bool the carrier of (InclPoset (Ids N))

union T is set

y is non empty directed lower Element of bool the carrier of N

BC is Element of the carrier of (InclPoset (Ids N))

BC is Element of the carrier of (InclPoset (Ids N))

N is non empty reflexive transitive non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

S is non empty directed Element of bool the carrier of (InclPoset (Ids N))

"\/" (S,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

union S is set

T is non empty directed lower Element of bool the carrier of N

y is Element of the carrier of (InclPoset (Ids N))

BC is Element of the carrier of (InclPoset (Ids N))

N is non empty reflexive transitive antisymmetric with_infima non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete with_infima non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

S is non empty directed Element of bool the carrier of (InclPoset (Ids N))

T is Element of the carrier of (InclPoset (Ids N))

{T} is non empty trivial finite 1 -element Element of bool the carrier of (InclPoset (Ids N))

{T} "/\" S is non empty Element of bool the carrier of (InclPoset (Ids N))

"\/" (({T} "/\" S),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

{ (T /\ b

union { (T /\ b

{ (T "/\" b

A is set

C is Element of the carrier of (InclPoset (Ids N))

T "/\" C is Element of the carrier of (InclPoset (Ids N))

A is Element of bool the carrier of (InclPoset (Ids N))

"\/" (A,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

"\/" (S,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

T "/\" ("\/" (S,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))

c

T /\ ("\/" (S,(InclPoset (Ids N)))) is set

union S is set

K is set

KK is Element of the carrier of (InclPoset (Ids N))

T /\ KK is set

C is set

c

K is Element of S

T /\ K is set

KK is Element of the carrier of (InclPoset (Ids N))

T "/\" KK is Element of the carrier of (InclPoset (Ids N))

T /\ KK is set

N is non empty reflexive transitive antisymmetric with_infima non void RelStr

Ids N is non empty set

the carrier of N is non empty set

bool the carrier of N is non empty set

{ b

InclPoset (Ids N) is non empty strict reflexive transitive antisymmetric up-complete with_infima non void RelStr

the carrier of (InclPoset (Ids N)) is non empty set

bool the carrier of (InclPoset (Ids N)) is non empty set

T is Element of the carrier of (InclPoset (Ids N))

{T} is non empty trivial finite 1 -element Element of bool the carrier of (InclPoset (Ids N))

y is non empty directed Element of bool the carrier of (InclPoset (Ids N))

"\/" (y,(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

T "/\" ("\/" (y,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))

{T} "/\" y is non empty Element of bool the carrier of (InclPoset (Ids N))

"\/" (({T} "/\" y),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

T "/\" ("\/" (y,(InclPoset (Ids N)))) is Element of the carrier of (InclPoset (Ids N))

T /\ ("\/" (y,(InclPoset (Ids N)))) is set

union y is set

T /\ (union y) is set

{ (T /\ b

union { (T /\ b

{T} "/\" y is non empty Element of bool the carrier of (InclPoset (Ids N))

"\/" (({T} "/\" y),(InclPoset (Ids N))) is Element of the carrier of (InclPoset (Ids N))

N is non empty trivial finite 1 -element RelStr

S is non empty TopAugmentation of N

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict RelStr

the carrier of N is non empty trivial finite 1 -element set

the InternalRel of N is Relation-like the carrier of N -defined the carrier of N -valued finite Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty finite set

bool [: the carrier of N, the carrier of N:] is non empty finite V32() set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict RelStr

N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr

the carrier of N is non empty set

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the topology of N is non empty Element of bool (bool the carrier of N)

bool the carrier of N is non empty set

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

TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) is strict TopRelStr

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of S is non empty set

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

the topology of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) is strict TopRelStr

sigma N is non empty Element of bool (bool the carrier of N)

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

sigma S is non empty Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

the carrier of N is non empty set

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the topology of N is non empty Element of bool (bool the carrier of N)

bool the carrier of N is non empty set

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

TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) is strict TopRelStr

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of S is non empty set

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of S

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

the topology of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) is strict TopRelStr

omega S is Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

omega N is Element of bool (bool the carrier of N)

the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S

the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S

the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set

the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:]

[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:] is non empty set

bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S:] is non empty set

RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set

the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:]

[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set

bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S:] is non empty set

RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S)

bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S is non empty set

bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S) is non empty set

the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S)

bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set

bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S) is non empty set

the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S \/ the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set

bool the carrier of N is non empty Element of bool (bool the carrier of N)

BC is set

BC is Element of bool (bool the carrier of N)

sigma N is non empty Element of bool (bool the carrier of N)

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)

sigma S is non empty Element of bool (bool the carrier of S)

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

(sigma S) \/ (omega N) is non empty set

the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of S \/ the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete lower non void TopAugmentation of S is non empty set

A is Element of bool (bool the carrier of N)

FinMeetCl A is Element of bool (bool the carrier of N)

UniCl (FinMeetCl A) is Element of bool (bool the carrier of N)

lambda S is Element of bool (bool the carrier of S)

RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N

the carrier of S is non empty set

bool the carrier of S is non empty set

T is Element of bool the carrier of N

y is Element of bool the carrier of S

[#] S is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of S

([#] S) \ y is Element of bool the carrier of S

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

[#] N is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) compact Element of bool the carrier of N

([#] N) \ T is Element of bool the carrier of N

N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr

lambda N is Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N

the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N)

the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set

bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set

bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N) is non empty set

InclPoset the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete distributive with_suprema with_infima complete non void RelStr

N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr

sigma N is non empty Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

InclPoset (sigma N) is non empty strict reflexive transitive antisymmetric non void RelStr

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

sigma N is non empty Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

InclPoset (sigma N) is non empty strict reflexive transitive antisymmetric non void RelStr

lambda N is non empty Element of bool (bool the carrier of N)

InclPoset (lambda N) is non empty strict reflexive transitive antisymmetric non void RelStr

the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N

the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N)

the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set

bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty set

bool (bool the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N) is non empty set

InclPoset the topology of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopAugmentation of N is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete distributive with_suprema with_infima complete non void RelStr

N is non empty reflexive non void RelStr

sigma N is Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

Scott-Convergence N is Relation-like M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

{ (b

S is set

{} N is empty proper V23() V27() finite V32() cardinal {} -element directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N

uparrow ({} N) is empty proper V23() V27() finite V32() cardinal {} -element directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of N

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

bool S is non empty set

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

lambda N is non empty Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

the topology of N is non empty Element of bool (bool the carrier of N)

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

sigma N is non empty Element of bool (bool the carrier of N)

the carrier of N is non empty set

bool the carrier of N is non empty set

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

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

lambda N is non empty Element of bool (bool the carrier of N)

{ (b

the topology of N is non empty Element of bool (bool the carrier of N)

N is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of N is non empty set

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of S is non empty set

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

lambda N is non empty Element of bool (bool the carrier of N)

bool the carrier of N is non empty set

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

lambda S is non empty Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

sigma S is non empty Element of bool (bool the carrier of S)

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

omega S is Element of bool (bool the carrier of S)

(sigma S) \/ (omega S) is non empty Element of bool (bool the carrier of S)

FinMeetCl ((sigma S) \/ (omega S)) is Element of bool (bool the carrier of S)

UniCl (FinMeetCl ((sigma S) \/ (omega S))) is Element of bool (bool the carrier of S)

sigma N is non empty Element of bool (bool the carrier of N)

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

omega N is Element of bool (bool the carrier of N)

(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)

FinMeetCl ((sigma N) \/ (omega N)) is Element of bool (bool the carrier of N)

UniCl (FinMeetCl ((sigma N) \/ (omega N))) is Element of bool (bool the carrier of N)

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

lambda N is non empty Element of bool (bool the carrier of N)

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

S is Element of bool the carrier of N

the topology of N is non empty Element of bool (bool the carrier of N)

N is non empty trivial finite 1 -element reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic satisfying_axiom_of_approximation continuous non void satisfying_MC meet-continuous TopRelStr

S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower topological_semilattice satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr

the carrier of S is non empty trivial finite 1 -element set

bool the carrier of S is non empty finite V32() set

T is trivial finite closed directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of S

N is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete non void TopRelStr

the carrier of N is non empty set

S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr

the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty trivial finite 1 -element set

the InternalRel of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty Relation-like the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S -defined the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S -valued finite Element of bool [: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:]

[: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:] is non empty finite set

bool [: the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S:] is non empty finite V32() set

RelStr(# the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S, the InternalRel of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_K algebraic arithmetic satisfying_axiom_of_approximation continuous non void RelStr

the topology of S is non empty finite V32() Element of bool (bool the carrier of S)

the carrier of S is non empty trivial finite 1 -element set

bool the carrier of S is non empty finite V32() set

bool (bool the carrier of S) is non empty finite V32() set

{{}, the carrier of S} is non empty finite V32() set

the topology of N is non empty Element of bool (bool the carrier of N)

bool the carrier of N is non empty set

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

the topology of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty finite V32() Element of bool (bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S)

bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S is non empty finite V32() set

bool (bool the carrier of the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopAugmentation of S) is non empty finite V32() set

lambda N is non empty Element of bool (bool the carrier of N)

sigma N is non empty Element of bool (bool the carrier of N)

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

omega N is Element of bool (bool the carrier of N)

(sigma N) \/ (omega N) is non empty Element of bool (bool the carrier of N)

FinMeetCl ((sigma N) \/ (omega N)) is Element of bool (bool the carrier of N)

UniCl (FinMeetCl ((sigma N) \/ (omega N))) is Element of bool (bool the carrier of N)

(omega N) \/ (sigma N) is non empty Element of bool (bool the carrier of N)

FinMeetCl ((omega N) \/ (sigma N)) is Element of bool (bool the carrier of N)

the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr

the non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 V72() anti-discrete reflexive transitive antisymmetric lower-bounded upper-bounded V155() connected up-complete /\-complete distributive V195() complemented with_suprema with_infima complete satisfying_axiom_K algebraic arithmetic strict lower Lawson topological_semilattice Scott satisfying_axiom_of_approximation continuous locally-compact non void compact satisfying_MC meet-continuous TopRelStr

F

the carrier of F

{ F

N is set

S is Element of the carrier of F

F

N is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void satisfying_MC meet-continuous RelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

S is Element of bool the carrier of N

uparrow S is upper Element of bool the carrier of N

T is non empty directed Element of bool the carrier of N

"\/" (T,N) is Element of the carrier of N

y is Element of the carrier of N

{y} is non empty trivial finite 1 -element Element of bool the carrier of N

{y} "/\" T is non empty Element of bool the carrier of N

"\/" (({y} "/\" T),N) is Element of the carrier of N

BC is non empty directed Element of bool the carrier of N

BC "/\" T is non empty directed Element of bool the carrier of N

BC is Element of the carrier of N

{ (y "/\" b

A is Element of the carrier of N

y "/\" A is Element of the carrier of N

C is Element of the carrier of N

N is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void satisfying_MC meet-continuous RelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

S is property(S) Element of bool the carrier of N

uparrow S is upper Element of bool the carrier of N

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

lambda N is non empty Element of bool (bool the carrier of N)

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

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N

sigma S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

T is Element of bool the carrier of N

uparrow T is upper Element of bool the carrier of N

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

y is Element of bool the carrier of S

uparrow y is upper Element of bool the carrier of S

BC is Element of bool the carrier of S

the topology of S is non empty Element of bool (bool the carrier of S)

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N

the carrier of S is non empty set

bool the carrier of S is non empty set

T is Element of bool the carrier of N

y is Element of bool the carrier of S

uparrow y is upper Element of bool the carrier of S

lambda N is non empty Element of bool (bool the carrier of N)

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

uparrow T is upper Element of bool the carrier of N

sigma S is non empty Element of bool (bool the carrier of S)

bool (bool the carrier of S) is non empty set

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

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

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

T is Element of the carrier of S

y is Element of the carrier of N

BC is non empty open y -quasi_basis Element of bool (bool the carrier of N)

{ (uparrow b

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

bool the carrier of S is non empty Element of bool (bool the carrier of S)

C is set

c

uparrow c

C is Element of bool (bool the carrier of S)

c

K is Element of bool the carrier of N

uparrow K is upper Element of bool the carrier of N

KK is Element of bool the carrier of S

uparrow KK is upper Element of bool the carrier of S

the topology of S is non empty Element of bool (bool the carrier of S)

c

K is Element of bool the carrier of N

uparrow K is upper Element of bool the carrier of N

Intersect BC is Element of bool the carrier of N

Intersect C is Element of bool the carrier of S

c

uparrow c

K is Element of bool the carrier of N

lambda N is non empty Element of bool (bool the carrier of N)

uparrow K is upper Element of bool the carrier of N

sigma S is non empty Element of bool (bool the carrier of S)

Scott-Convergence S is Relation-like V246(S) V247(S) M36(S)

K403(S,(Scott-Convergence S)) is non empty strict TopSpace-like TopStruct

the topology of K403(S,(Scott-Convergence S)) is non empty Element of bool (bool the carrier of K403(S,(Scott-Convergence S)))

the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool the carrier of K403(S,(Scott-Convergence S)) is non empty set

bool (bool the carrier of K403(S,(Scott-Convergence S))) is non empty set

sigma N is non empty Element of bool (bool the carrier of N)

Scott-Convergence N is Relation-like V246(N) V247(N) M36(N)

K403(N,(Scott-Convergence N)) is non empty strict TopSpace-like TopStruct

the topology of K403(N,(Scott-Convergence N)) is non empty Element of bool (bool the carrier of K403(N,(Scott-Convergence N)))

the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool the carrier of K403(N,(Scott-Convergence N)) is non empty set

bool (bool the carrier of K403(N,(Scott-Convergence N))) is non empty set

KK is Element of bool the carrier of N

uparrow KK is upper Element of bool the carrier of N

c

N is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Lawson non void compact satisfying_MC meet-continuous TopRelStr

the carrier of N is non empty set

bool the carrier of N is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete Scott non void TopAugmentation of N

the carrier of S is non empty set

bool the carrier of S is non empty set

T is upper Element of bool the carrier of N

Int T is open Element of bool the carrier of N

y is Element of bool the carrier of S

Int y is open Element of bool the carrier of S

the InternalRel of N is non empty Relation-like the carrier of N -defined the carrier of N -valued Element of bool [: the carrier of N, the carrier of N:]

[: the carrier of N, the carrier of N:] is non empty set

bool [: the carrier of N, the carrier of N:] is non empty set

RelStr(# the carrier of N, the InternalRel of N #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima non void RelStr

uparrow (Int T) is upper Element of bool the carrier of N

BC is Element of bool the carrier of S

A is set

uparrow T is upper Element of bool the carrier of N

C is Element of the carrier of N

c

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