:: WAYBEL19 semantic presentation

K256() is Element of bool K252()
K252() is set
bool K252() is non empty set
K87() is set
bool K87() is non empty set
K181() is non empty strict TopSpace-like TopStruct
the carrier of K181() is non empty set
{} is empty finite V32() set
the empty finite V32() set is empty finite V32() set
1 is non empty set
{{},1} is non empty finite set
bool K256() is non empty set
{{}} is non empty finite V32() set
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty RelStr
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of x : verum } is set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
y9 is set
u is Element of the carrier of T
uparrow u is Element of bool the carrier of T
bool the carrier of T is non empty set
{u} is non empty finite Element of bool the carrier of T
uparrow {u} is Element of bool the carrier of T
(uparrow u) ` is Element of bool the carrier of T
the carrier of T \ (uparrow u) is set
W is Element of the carrier of x
uparrow W is Element of bool the carrier of x
bool the carrier of x is non empty set
{W} is non empty finite Element of bool the carrier of x
uparrow {W} is Element of bool the carrier of x
(uparrow W) ` is Element of bool the carrier of x
the carrier of x \ (uparrow W) is set
y9 is set
u is Element of the carrier of x
uparrow u is Element of bool the carrier of x
{u} is non empty finite Element of bool the carrier of x
uparrow {u} is Element of bool the carrier of x
(uparrow u) ` is Element of bool the carrier of x
the carrier of x \ (uparrow u) is set
W is Element of the carrier of T
uparrow W is Element of bool the carrier of T
{W} is non empty finite Element of bool the carrier of T
uparrow {W} is Element of bool the carrier of T
(uparrow W) ` is Element of bool the carrier of T
the carrier of T \ (uparrow W) is set
T is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete non void TopRelStr
the carrier of T is non empty trivial finite set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
bool the carrier of T is non empty finite V32() set
bool (bool the carrier of T) is non empty finite V32() set
{ the carrier of T} is non empty finite V32() set
bool the carrier of T is non empty finite V32() Element of bool (bool the carrier of T)
x9 is set
y9 is Element of the carrier of T
uparrow y9 is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
{y9} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T
uparrow {y9} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
(uparrow y9) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T
the carrier of T \ (uparrow y9) is finite set
x9 is finite V32() Element of bool (bool the carrier of T)
the Element of the carrier of T is Element of the carrier of T
W is set
V is Element of the carrier of T
uparrow V is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
{V} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T
uparrow {V} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
(uparrow V) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T
the carrier of T \ (uparrow V) is finite set
uparrow the Element of the carrier of T is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
{ the Element of the carrier of T} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T
uparrow { the Element of the carrier of T} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
(uparrow the Element of the carrier of T) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T
the carrier of T \ (uparrow the Element of the carrier of T) is finite set
y9 is finite V32() Element of bool (bool the carrier of T)
FinMeetCl y9 is finite V32() Element of bool (bool the carrier of T)
{{}, the carrier of T} is non empty finite V32() set
y is non empty finite V32() V69(T) quasi_basis Element of bool (bool the carrier of T)
the topology of T is non empty finite V32() Element of bool (bool the carrier of T)
u is set
W is Element of the carrier of T
uparrow W is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
{W} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T
uparrow {W} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
(uparrow W) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T
the carrier of T \ (uparrow W) is finite set
V is set
(uparrow W) /\ u is trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T
the non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete strict non void () TopRelStr is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete strict non void () TopRelStr
T is non empty RelStr
the carrier of T is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
bool the carrier 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
y is set
x9 is Element of the carrier of T
uparrow x9 is Element of bool the carrier of T
{x9} is non empty finite Element of bool the carrier of T
uparrow {x9} is Element of bool the carrier of T
(uparrow x9) ` is Element of bool the carrier of T
the carrier of T \ (uparrow x9) is set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
y is Element of bool (bool the carrier of T)
FinMeetCl y is Element of bool (bool the carrier of T)
UniCl (FinMeetCl y) is Element of bool (bool the carrier of T)
TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is strict TopRelStr
TopStruct(# the carrier of T,(UniCl (FinMeetCl y)) #) is non empty strict TopStruct
the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is set
the topology of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is Element of bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #))
bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is non empty set
bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)) is non empty set
TopStruct(# the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #), the topology of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) #) is strict TopStruct
y9 is non empty TopSpace-like TopStruct
the carrier of y9 is non empty set
bool the carrier of y9 is non empty set
bool (bool the carrier of y9) is non empty set
u is Element of bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #))
W is Element of bool (bool the carrier of y9)
union W is Element of bool the carrier of y9
the topology of y9 is non empty Element of bool (bool the carrier of y9)
union u is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)
u is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)
W is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)
u /\ W is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)
u is non empty TopSpace-like strict TopRelStr
the carrier of u is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of u : verum } is set
the InternalRel of u is Relation-like the carrier of u -defined the carrier of u -valued Element of bool [: the carrier of u, the carrier of u:]
[: the carrier of u, the carrier of u:] is non empty set
bool [: the carrier of u, the carrier of u:] is non empty set
RelStr(# the carrier of u, the InternalRel of u #) is strict RelStr
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of y9 is non empty set
bool the carrier of y9 is non empty set
bool (bool the carrier of y9) is non empty set
V is non empty V69(y9) quasi_basis Element of bool (bool the carrier of y9)
the topology of u is non empty Element of bool (bool the carrier of u)
bool the carrier of u is non empty set
bool (bool the carrier of u) is non empty set
UniCl V is Element of bool (bool the carrier of y9)
the topology of y9 is non empty Element of bool (bool the carrier of y9)
T is non empty RelStr
T is non empty TopSpace-like () TopRelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty TopSpace-like () TopRelStr
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
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
the topology of x is non empty Element of bool (bool the carrier of x)
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of x : verum } is set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T
y is Element of bool (bool the carrier of T)
x9 is Element of bool (bool the carrier of T)
the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)
the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set
the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T
the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like () TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like () TopAugmentation of T -defined the carrier of the non empty TopSpace-like () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like () TopAugmentation of T, the InternalRel of the non empty TopSpace-like () TopAugmentation of T #) is strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set
y is Element of bool (bool the carrier of T)
x9 is non empty TopSpace-like () TopAugmentation of T
the topology of x9 is non empty Element of bool (bool the carrier of x9)
the carrier of x9 is non empty set
bool the carrier of x9 is non empty set
bool (bool the carrier of x9) is non empty set
the InternalRel of x9 is Relation-like the carrier of x9 -defined the carrier of x9 -valued Element of bool [: the carrier of x9, the carrier of x9:]
[: the carrier of x9, the carrier of x9:] is non empty set
bool [: the carrier of x9, the carrier of x9:] is non empty set
RelStr(# the carrier of x9, the InternalRel of x9 #) is strict RelStr
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty RelStr
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
(T) is 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
(x) is Element of bool (bool the carrier of x)
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T
the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like () TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like () TopAugmentation of T -defined the carrier of the non empty TopSpace-like () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like () TopAugmentation of T, the InternalRel of the non empty TopSpace-like () TopAugmentation of T #) is strict RelStr
the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set
T is non empty () TopRelStr
the carrier of T is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
y is Element of the carrier of T
uparrow y is Element of bool the carrier of T
bool the carrier of T is non empty set
{y} is non empty finite Element of bool the carrier of T
uparrow {y} is Element of bool the carrier of T
(uparrow y) ` is Element of bool the carrier of T
the carrier of T \ (uparrow y) is set
bool (bool the carrier of T) is non empty set
the topology of T is Element of bool (bool the carrier of T)
x9 is Element of the carrier of T
uparrow x9 is Element of bool the carrier of T
{x9} is non empty finite Element of bool the carrier of T
uparrow {x9} is Element of bool the carrier of T
(uparrow x9) ` is Element of bool the carrier of T
the carrier of T \ (uparrow x9) is set
[#] T is non empty non proper dense lower upper Element of bool the carrier of T
([#] T) \ (uparrow y) is Element of bool the carrier of T
T is non empty transitive () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
y is Element of bool the carrier of T
the topology of T is Element of bool (bool the carrier of T)
x9 is Element of the carrier of T
y9 is Element of the carrier of T
x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
FinMeetCl x is Element of bool (bool the carrier of T)
u is V69(T) quasi_basis Element of bool (bool the carrier of T)
UniCl u is Element of bool (bool the carrier of T)
W is Element of bool (bool the carrier of T)
union W is Element of bool the carrier of T
V is set
x is Element of bool (bool the carrier of T)
Intersect x is Element of bool the carrier of T
z is set
Y is Element of the carrier of T
uparrow Y is upper Element of bool the carrier of T
{Y} is non empty finite Element of bool the carrier of T
uparrow {Y} is upper Element of bool the carrier of T
(uparrow Y) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow Y) is set
(uparrow Y) /\ z is Element of bool the carrier of T
{} T is empty proper finite V32() boundary directed filtered lower upper Element of bool the carrier of T
T is non empty transitive () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is Element of bool the carrier of T
[#] T is non empty non proper dense lower upper Element of bool the carrier of T
([#] T) \ x is Element of bool the carrier of T
the topology of T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
x ` is Element of bool the carrier of T
the carrier of T \ x is set
y is Element of the carrier of T
x9 is Element of the carrier of T
T is non empty TopSpace-like TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of bool the carrier of T : b<sub>1</sub> is finite } is set
bool (bool the carrier of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
y is set
x9 is Element of the carrier of T
uparrow x9 is Element of bool the carrier of T
{x9} is non empty finite compact Element of bool the carrier of T
uparrow {x9} is Element of bool the carrier of T
(uparrow x9) ` is Element of bool the carrier of T
the carrier of T \ (uparrow x9) is set
y is Element of bool (bool the carrier of T)
u is Element of bool (bool the carrier of T)
FinMeetCl u is Element of bool (bool the carrier of T)
x9 is non empty RelStr
the carrier of x9 is non empty set
bool the carrier of x9 is non empty set
W is set
V is Element of bool the carrier of T
uparrow V is Element of bool the carrier of T
(uparrow V) ` is Element of bool the carrier of T
the carrier of T \ (uparrow V) is set
{ (uparrow b₁) where b₁ is Element of the carrier of T : b₁ in V } is set
z is set
Y is Element of the carrier of T
uparrow Y is Element of bool the carrier of T
{Y} is non empty finite compact Element of bool the carrier of T
uparrow {Y} is Element of bool the carrier of T
z is Element of bool (bool the carrier of T)
Y is Element of bool (bool the carrier of T)
union Y is Element of bool the carrier of T
COMPLEMENT Y is Element of bool (bool the carrier of T)
Intersect (COMPLEMENT Y) is Element of bool the carrier of T
bool (bool the carrier of x9) is non empty set
I2 is Element of bool (bool the carrier of x9)
{ H₂(b₁) where b₁ is Element of the carrier of x9 : b₁ in V } is set
COMPLEMENT I2 is Element of bool (bool the carrier of x9)
{ (H₂(b₁) `) where b<sub>1</sub> is Element of the carrier of x9 : b<sub>1</sub> in V } is set
Y is set
Z is Element of the carrier of T
uparrow Z is Element of bool the carrier of T
{Z} is non empty finite compact Element of bool the carrier of T
uparrow {Z} is Element of bool the carrier of T
(uparrow Z) ` is Element of bool the carrier of T
the carrier of T \ (uparrow Z) is set
{ H₃(b₁) where b₁ is Element of the carrier of T : b₁ in V } is set
W is set
V is Element of bool (bool the carrier of T)
Intersect V is Element of bool the carrier of T
x is set
z is Element of the carrier of T
uparrow z is Element of bool the carrier of T
{z} is non empty finite compact Element of bool the carrier of T
uparrow {z} is Element of bool the carrier of T
(uparrow z) ` is Element of bool the carrier of T
the carrier of T \ (uparrow z) is set
x is Relation-like Function-like set
dom x is set
rng x is set
z is Element of bool the carrier of T
{ (uparrow b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of T : b<sub>1</sub> in z } is set
I2 is set
Y is Element of the carrier of T
uparrow Y is Element of bool the carrier of T
{Y} is non empty finite compact Element of bool the carrier of T
uparrow {Y} is Element of bool the carrier of T
I2 is Element of bool (bool the carrier of T)
Y is Element of bool (bool the carrier of T)
Z is Element of bool (bool the carrier of x9)
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of x9 : b<sub>1</sub> in z } is set
COMPLEMENT Z is Element of bool (bool the carrier of x9)
{ (H<sub>1</sub>(b<sub>1</sub>) `) where b₁ is Element of the carrier of x9 : b₁ in z } is set
COMPLEMENT Y is Element of bool (bool the carrier of T)
J2 is set
y is Element of the carrier of x9
uparrow y is Element of bool the carrier of x9
{y} is non empty finite Element of bool the carrier of x9
uparrow {y} is Element of bool the carrier of x9
(uparrow y) ` is Element of bool the carrier of x9
the carrier of x9 \ (uparrow y) is set
a is set
x . a is set
AA is Element of the carrier of T
uparrow AA is Element of bool the carrier of T
{AA} is non empty finite compact Element of bool the carrier of T
uparrow {AA} is Element of bool the carrier of T
(uparrow AA) ` is Element of bool the carrier of T
the carrier of T \ (uparrow AA) is set
J2 is set
x . J2 is set
y is Element of the carrier of T
uparrow y is Element of bool the carrier of T
{y} is non empty finite compact Element of bool the carrier of T
uparrow {y} is Element of bool the carrier of T
(uparrow y) ` is Element of bool the carrier of T
the carrier of T \ (uparrow y) is set
uparrow z is Element of bool the carrier of T
union Y is Element of bool the carrier of T
(uparrow z) ` is Element of bool the carrier of T
the carrier of T \ (uparrow z) is set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of x is non empty set
[: the carrier of T, the carrier of x:] is non empty set
bool [: the carrier of T, the carrier of x:] is non empty set
bool the carrier of T is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of x : verum } is set
x9 is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]
y9 is Element of bool the carrier of x
y9 ` is Element of bool the carrier of x
the carrier of x \ y9 is set
x9 " (y9 `) is Element of bool the carrier of T
x9 .: (x9 " (y9 `)) is Element of bool the carrier of x
y is V69(x) quasi_prebasis Element of bool (bool the carrier of x)
u is Element of the carrier of x
uparrow u is non empty filtered upper Element of bool the carrier of x
{u} is non empty finite compact Element of bool the carrier of x
uparrow {u} is non empty upper Element of bool the carrier of x
(uparrow u) ` is lower property(S) Element of bool the carrier of x
the carrier of x \ (uparrow u) is set
x9 " (uparrow u) is Element of bool the carrier of T
"/\" ((x9 " (uparrow u)),T) is Element of the carrier of T
{} T is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of T
x9 . ("/\" ((x9 " (uparrow u)),T)) is Element of the carrier of x
"/\" ((x9 .: (x9 " (y9 `))),x) is Element of the carrier of x
"/\" ((y9 `),x) is Element of the carrier of x
uparrow ("/\" ((x9 " (uparrow u)),T)) is non empty filtered upper Element of bool the carrier of T
{("/\" ((x9 " (uparrow u)),T))} is non empty finite compact Element of bool the carrier of T
uparrow {("/\" ((x9 " (uparrow u)),T))} is non empty upper Element of bool the carrier of T
V is set
x is Element of the carrier of T
V is set
x is Element of the carrier of T
{("/\" ((x9 " (uparrow u)),T)),x} is non empty finite Element of bool the carrier of T
("/\" ((x9 " (uparrow u)),T)) "/\" x is Element of the carrier of T
x9 . (("/\" ((x9 " (uparrow u)),T)) "/\" x) is Element of the carrier of x
x9 . x is Element of the carrier of x
(x9 . ("/\" ((x9 " (uparrow u)),T))) "/\" (x9 . x) is Element of the carrier of x
{} T is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of x is non empty set
[: the carrier of T, the carrier of x:] is non empty set
bool [: the carrier of T, the carrier of x:] is non empty set
y is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]
bool the carrier of T is non empty set
x9 is non empty Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
y is non empty filtered Element of bool the carrier of T
"/\" (y,T) is Element of the carrier of T
Cl y is closed Element of bool the carrier of T
y opp+id is non empty reflexive transitive strict directed non void NetStr over T
subrelstr y is strict reflexive transitive antisymmetric full SubRelStr of T
K448(T,(subrelstr y)) is Relation-like the carrier of (subrelstr y) -defined the carrier of T -valued Function-like V18( the carrier of (subrelstr y), the carrier of T) Element of bool [: the carrier of (subrelstr y), the carrier of T:]
the carrier of (subrelstr y) is set
[: the carrier of (subrelstr y), the carrier of T:] is set
bool [: the carrier of (subrelstr y), the carrier of T:] is non empty set
(subrelstr y) opp+id is strict strict directed NetStr over subrelstr y
K448(T,(subrelstr y)) * ((subrelstr y) opp+id) is strict NetStr over T
u is Element of bool the carrier of T
W is set
the carrier of (y opp+id) is non empty set
V is Element of the carrier of (y opp+id)
x is Element of the carrier of (y opp+id)
(y opp+id) . x is Element of the carrier of T
the mapping of (y opp+id) is non empty Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]
[: the carrier of (y opp+id), the carrier of T:] is non empty set
bool [: the carrier of (y opp+id), the carrier of T:] is non empty set
K76( the carrier of (y opp+id), the carrier of T, the mapping of (y opp+id),x) is Element of the carrier of T
T ~ is non empty strict reflexive transitive antisymmetric non void RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
the carrier of (T ~) is non empty set
z is Element of the carrier of (T ~)
Y is Element of the carrier of (T ~)
~ Y is Element of the carrier of T
~ z is Element of the carrier of T
the carrier of (y opp+id) is non empty set
netmap ((y opp+id),T) is Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]
[: the carrier of (y opp+id), the carrier of T:] is non empty set
bool [: the carrier of (y opp+id), the carrier of T:] is non empty set
the mapping of (y opp+id) is non empty Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]
rng (netmap ((y opp+id),T)) is Element of bool the carrier of T
u is set
dom (netmap ((y opp+id),T)) is Element of bool the carrier of (y opp+id)
bool the carrier of (y opp+id) is non empty set
W is set
(netmap ((y opp+id),T)) . W is set
V is Element of the carrier of (y opp+id)
(y opp+id) . V is Element of the carrier of T
K76( the carrier of (y opp+id), the carrier of T, the mapping of (y opp+id),V) is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of x is non empty set
[: the carrier of T, the carrier of x:] is non empty set
bool [: the carrier of T, the carrier of x:] is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
x9 is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]
y9 is Element of bool the carrier of T
x9 .: y9 is Element of bool the carrier of x
bool the carrier of x is non empty set
"/\" ((x9 .: y9),x) is Element of the carrier of x
"/\" (y9,T) is Element of the carrier of T
K76( the carrier of T, the carrier of x,x9,("/\" (y9,T))) is Element of the carrier of x
y is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
u is Element of bool the carrier of T
W is Element of the carrier of T
uparrow W is non empty filtered upper Element of bool the carrier of T
{W} is non empty finite compact Element of bool the carrier of T
uparrow {W} is non empty upper Element of bool the carrier of T
(uparrow W) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow W) is set
V is Element of the carrier of T
Cl y9 is closed Element of bool the carrier of T
u is Element of the carrier of T
W is Element of the carrier of T
K76( the carrier of T, the carrier of x,x9,u) is Element of the carrier of x
K76( the carrier of T, the carrier of x,x9,W) is Element of the carrier of x
x9 . u is Element of the carrier of x
uparrow (x9 . u) is non empty filtered upper Element of bool the carrier of x
{(x9 . u)} is non empty finite compact Element of bool the carrier of x
uparrow {(x9 . u)} is non empty upper Element of bool the carrier of x
x9 " (uparrow (x9 . u)) is Element of bool the carrier of T
x9 . W is Element of the carrier of x
x9 . ("/\" (y9,T)) is Element of the carrier of x
u is Element of the carrier of x
W is set
x9 . W is set
V is Element of the carrier of T
uparrow ("/\" ((x9 .: y9),x)) is non empty filtered upper Element of bool the carrier of x
{("/\" ((x9 .: y9),x))} is non empty finite compact Element of bool the carrier of x
uparrow {("/\" ((x9 .: y9),x))} is non empty upper Element of bool the carrier of x
x9 " (uparrow ("/\" ((x9 .: y9),x))) is Element of bool the carrier of T
u is set
W is Element of the carrier of T
x9 . W is Element of the carrier of x
Cl (x9 " (uparrow ("/\" ((x9 .: y9),x)))) is closed Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of x is non empty set
[: the carrier of T, the carrier of x:] is non empty set
bool [: the carrier of T, the carrier of x:] is non empty set
bool the carrier of T is non empty set
y is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]
x9 is non empty filtered Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive non void () TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite compact Element of bool the carrier of T
bool the carrier of T is non empty set
Cl {x} is closed Element of bool the carrier of T
uparrow x is non empty filtered upper Element of bool the carrier of T
uparrow {x} is non empty upper Element of bool the carrier of T
y is Element of the carrier of T
uparrow (Cl {x}) is upper Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric non void TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
y is Element of the carrier of T
x9 is Element of the carrier of T
uparrow x9 is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{x9} is non empty finite compact Element of bool the carrier of T
uparrow {x9} is non empty upper Element of bool the carrier of T
(uparrow x9) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow x9) is set
y9 is Element of the carrier of T
uparrow y9 is non empty filtered upper Element of bool the carrier of T
{y9} is non empty finite compact Element of bool the carrier of T
uparrow {y9} is non empty upper Element of bool the carrier of T
(uparrow y9) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow y9) is set
T is non empty lower-bounded RelStr
x is non empty TopAugmentation of T
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
T is non empty RelStr
the carrier of T is non empty set
x is non empty RelStr
the carrier of x is non empty set
[:T,x:] is non empty strict RelStr
the carrier of [:T,x:] is non empty set
y is Element of the carrier of T
uparrow y is Element of bool the carrier of T
bool the carrier of T is non empty set
{y} is non empty finite Element of bool the carrier of T
uparrow {y} is Element of bool the carrier of T
(uparrow y) ` is Element of bool the carrier of T
the carrier of T \ (uparrow y) is set
[:((uparrow y) `), the carrier of x:] is set
x9 is Element of the carrier of x
[y,x9] is Element of the carrier of [:T,x:]
{y,x9} is non empty finite set
{y} is non empty finite set
{{y,x9},{y}} is non empty finite V32() set
uparrow [y,x9] is Element of bool the carrier of [:T,x:]
bool the carrier of [:T,x:] is non empty set
{[y,x9]} is non empty finite Element of bool the carrier of [:T,x:]
uparrow {[y,x9]} is Element of bool the carrier of [:T,x:]
(uparrow [y,x9]) ` is Element of bool the carrier of [:T,x:]
the carrier of [:T,x:] \ (uparrow [y,x9]) is set
uparrow x9 is Element of bool the carrier of x
bool the carrier of x is non empty set
{x9} is non empty finite Element of bool the carrier of x
uparrow {x9} is Element of bool the carrier of x
(uparrow x9) ` is Element of bool the carrier of x
the carrier of x \ (uparrow x9) is set
[: the carrier of T,((uparrow x9) `):] is set
[:((uparrow y) `), the carrier of x:] \/ [: the carrier of T,((uparrow x9) `):] is set
[: the carrier of T, the carrier of x:] is non empty set
[: the carrier of T, the carrier of x:] \ (uparrow [y,x9]) is Relation-like the carrier of T -defined the carrier of x -valued Element of bool [: the carrier of T, the carrier of x:]
bool [: the carrier of T, the carrier of x:] is non empty set
[:(uparrow y),(uparrow x9):] is Element of bool the carrier of [:T,x:]
[: the carrier of T, the carrier of x:] \ [:(uparrow y),(uparrow x9):] is Relation-like the carrier of T -defined the carrier of x -valued Element of bool [: the carrier of T, the carrier of x:]
T is non empty reflexive transitive antisymmetric lower-bounded non void RelStr
x is non empty reflexive transitive antisymmetric lower-bounded non void RelStr
[:T,x:] is non empty strict reflexive transitive antisymmetric non void RelStr
([:T,x:]) is Element of bool (bool the carrier of [:T,x:])
the carrier of [:T,x:] is non empty set
bool the carrier of [:T,x:] is non empty set
bool (bool the carrier of [:T,x:]) is non empty set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] : verum } is set
y9 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopAugmentation of T
the carrier of y9 is non empty set
bool the carrier of y9 is non empty set
bool (bool the carrier of y9) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of y9 : verum } is set
W is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopAugmentation of x
[:y9,W:] is non empty strict TopSpace-like TopStruct
the topology of [:y9,W:] is non empty Element of bool (bool the carrier of [:y9,W:])
the carrier of [:y9,W:] is non empty set
bool the carrier of [:y9,W:] is non empty set
bool (bool the carrier of [:y9,W:]) is non empty set
the carrier of W is non empty set
u is V69(y9) quasi_prebasis Element of bool (bool the carrier of y9)
{ [:b₁, the carrier of W:] where b₁ is Element of bool the carrier of y9 : b₁ in u } is set
the InternalRel of W is non empty Relation-like the carrier of W -defined the carrier of W -valued Element of bool [: the carrier of W, the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
bool [: the carrier of W, the carrier of W:] is non empty set
RelStr(# the carrier of W, the InternalRel of W #) is strict RelStr
the carrier of x is non empty set
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
bool the carrier of W is non empty set
bool (bool the carrier of W) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of W : verum } is set
the InternalRel of y9 is non empty Relation-like the carrier of y9 -defined the carrier of y9 -valued Element of bool [: the carrier of y9, the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is non empty set
bool [: the carrier of y9, the carrier of y9:] is non empty set
RelStr(# the carrier of y9, the InternalRel of y9 #) is strict 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
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
[: the carrier of T, the carrier of x:] is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] #) is strict RelStr
x9 is V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])
Y is set
[#] W is non empty non proper open closed dense non boundary filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of W
I2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow I2 is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
{I2} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow {I2} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
(uparrow I2) ` is lower Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] \ (uparrow I2) is set
Y is set
Z is set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty finite set
{{Y,Z},{Y}} is non empty finite V32() set
y is Element of the carrier of T
J2 is Element of the carrier of x
[y,J2] is Element of the carrier of [:T,x:]
{y,J2} is non empty finite set
{y} is non empty finite set
{{y,J2},{y}} is non empty finite V32() set
uparrow [y,J2] is non empty filtered upper Element of bool the carrier of [:T,x:]
{[y,J2]} is non empty finite Element of bool the carrier of [:T,x:]
uparrow {[y,J2]} is non empty upper Element of bool the carrier of [:T,x:]
uparrow y is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{y} is non empty finite Element of bool the carrier of T
uparrow {y} is non empty upper Element of bool the carrier of T
(uparrow y) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow y) is set
[#] x is non empty non proper filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of x
bool the carrier of x is non empty set
[:((uparrow y) `),([#] x):] is lower Element of bool the carrier of [:T,x:]
[#] T is non empty non proper filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of T
uparrow J2 is non empty filtered upper Element of bool the carrier of x
{J2} is non empty finite Element of bool the carrier of x
uparrow {J2} is non empty upper Element of bool the carrier of x
(uparrow J2) ` is lower Element of bool the carrier of x
the carrier of x \ (uparrow J2) is set
[:([#] T),((uparrow J2) `):] is lower Element of bool the carrier of [:T,x:]
[:((uparrow y) `),([#] x):] \/ [:([#] T),((uparrow J2) `):] is Element of bool the carrier of [:T,x:]
AA is Element of the carrier of W
uparrow AA is non empty filtered upper Element of bool the carrier of W
{AA} is non empty finite compact Element of bool the carrier of W
uparrow {AA} is non empty upper Element of bool the carrier of W
(uparrow AA) ` is lower Element of bool the carrier of W
the carrier of W \ (uparrow AA) is set
z is V69(W) quasi_prebasis Element of bool (bool the carrier of W)
[#] y9 is non empty non proper open closed dense non boundary filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of y9
a is Element of the carrier of y9
uparrow a is non empty filtered upper Element of bool the carrier of y9
{a} is non empty finite compact Element of bool the carrier of y9
uparrow {a} is non empty upper Element of bool the carrier of y9
(uparrow a) ` is lower Element of bool the carrier of y9
the carrier of y9 \ (uparrow a) is set
G is Element of bool the carrier of [:y9,W:]
G is Element of bool the carrier of [:y9,W:]
G \/ G is Element of bool the carrier of [:y9,W:]
z is V69(W) quasi_prebasis Element of bool (bool the carrier of W)
{ [: the carrier of y9,b₁:] where b₁ is Element of bool the carrier of W : b₁ in z } is set
{ [: the carrier of y9,b₁:] where b₁ is Element of bool the carrier of W : b₁ in z } \/ { [:b₁, the carrier of W:] where b₁ is Element of bool the carrier of y9 : b₁ in u } is set
UniCl the topology of [:y9,W:] is Element of bool (bool the carrier of [:y9,W:])
I2 is V69([:y9,W:]) quasi_prebasis Element of bool (bool the carrier of [:y9,W:])
Y is set
Z is Element of bool the carrier of W
[: the carrier of y9,Z:] is set
J2 is Element of the carrier of W
uparrow J2 is non empty filtered upper Element of bool the carrier of W
{J2} is non empty finite compact Element of bool the carrier of W
uparrow {J2} is non empty upper Element of bool the carrier of W
(uparrow J2) ` is lower Element of bool the carrier of W
the carrier of W \ (uparrow J2) is set
Bottom T is Element of the carrier of T
y is Element of the carrier of x
[(Bottom T),y] is Element of the carrier of [:T,x:]
{(Bottom T),y} is non empty finite set
{(Bottom T)} is non empty finite set
{{(Bottom T),y},{(Bottom T)}} is non empty finite V32() set
a is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow a is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
{a} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow {a} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow [(Bottom T),y] is non empty filtered upper Element of bool the carrier of [:T,x:]
{[(Bottom T),y]} is non empty finite Element of bool the carrier of [:T,x:]
uparrow {[(Bottom T),y]} is non empty upper Element of bool the carrier of [:T,x:]
uparrow (Bottom T) is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{(Bottom T)} is non empty finite Element of bool the carrier of T
uparrow {(Bottom T)} is non empty upper Element of bool the carrier of T
(uparrow (Bottom T)) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow (Bottom T)) is set
uparrow y is non empty filtered upper Element of bool the carrier of x
bool the carrier of x is non empty set
{y} is non empty finite Element of bool the carrier of x
uparrow {y} is non empty upper Element of bool the carrier of x
(uparrow [(Bottom T),y]) ` is lower Element of bool the carrier of [:T,x:]
the carrier of [:T,x:] \ (uparrow [(Bottom T),y]) is set
[:{}, the carrier of x:] is set
[: the carrier of T,Z:] is set
[:{}, the carrier of x:] \/ [: the carrier of T,Z:] is set
{} \/ [: the carrier of T,Z:] is set
Z is Element of bool the carrier of y9
[:Z, the carrier of W:] is set
J2 is Element of the carrier of y9
uparrow J2 is non empty filtered upper Element of bool the carrier of y9
{J2} is non empty finite compact Element of bool the carrier of y9
uparrow {J2} is non empty upper Element of bool the carrier of y9
(uparrow J2) ` is lower Element of bool the carrier of y9
the carrier of y9 \ (uparrow J2) is set
y is Element of the carrier of T
Bottom x is Element of the carrier of x
[y,(Bottom x)] is Element of the carrier of [:T,x:]
{y,(Bottom x)} is non empty finite set
{y} is non empty finite set
{{y,(Bottom x)},{y}} is non empty finite V32() set
a is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow a is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
{a} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow {a} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]
uparrow [y,(Bottom x)] is non empty filtered upper Element of bool the carrier of [:T,x:]
{[y,(Bottom x)]} is non empty finite Element of bool the carrier of [:T,x:]
uparrow {[y,(Bottom x)]} is non empty upper Element of bool the carrier of [:T,x:]
uparrow (Bottom x) is non empty filtered upper Element of bool the carrier of x
bool the carrier of x is non empty set
{(Bottom x)} is non empty finite Element of bool the carrier of x
uparrow {(Bottom x)} is non empty upper Element of bool the carrier of x
(uparrow (Bottom x)) ` is lower Element of bool the carrier of x
the carrier of x \ (uparrow (Bottom x)) is set
uparrow y is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{y} is non empty finite Element of bool the carrier of T
uparrow {y} is non empty upper Element of bool the carrier of T
(uparrow [y,(Bottom x)]) ` is lower Element of bool the carrier of [:T,x:]
the carrier of [:T,x:] \ (uparrow [y,(Bottom x)]) is set
[:Z, the carrier of x:] is set
[: the carrier of T,{}:] is set
[:Z, the carrier of x:] \/ [: the carrier of T,{}:] is set
[:Z, the carrier of x:] \/ {} is set
FinMeetCl I2 is Element of bool (bool the carrier of [:y9,W:])
FinMeetCl x9 is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])
UniCl (FinMeetCl I2) is Element of bool (bool the carrier of [:y9,W:])
UniCl (FinMeetCl x9) is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])
FinMeetCl the topology of [:y9,W:] is Element of bool (bool the carrier of [:y9,W:])
T is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopRelStr
x is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopRelStr
[:T,x:] is non empty strict reflexive transitive antisymmetric non void RelStr
([:T,x:]) is Element of bool (bool the carrier of [:T,x:])
the carrier of [:T,x:] is non empty set
bool the carrier of [:T,x:] is non empty set
bool (bool the carrier of [:T,x:]) is non empty set
[:T,x:] is non empty strict TopSpace-like TopStruct
the topology of [:T,x:] is non empty Element of bool (bool the carrier of [:T,x:])
the carrier of [:T,x:] is non empty set
bool the carrier of [:T,x:] is non empty set
bool (bool the carrier of [:T,x:]) is non empty set
x is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
[:T,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the carrier of x is non empty set
the carrier of T is non empty set
[: the carrier of x, the carrier of T:] is non empty set
bool [: the carrier of x, the carrier of T:] is non empty set
inf_op T is Relation-like the carrier of [:T,T:] -defined the carrier of T -valued Function-like V18( the carrier of [:T,T:], the carrier of T) infs-preserving meet-preserving filtered-infs-preserving Element of bool [: the carrier of [:T,T:], the carrier of T:]
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:], the carrier of T:] is non empty set
bool [: the carrier of [:T,T:], the carrier of T:] is non empty set
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of [:T,T:] is non empty Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -valued Element of bool [: the carrier of [:T,T:], the carrier of [:T,T:]:]
[: the carrier of [:T,T:], the carrier of [:T,T:]:] is non empty set
bool [: the carrier of [:T,T:], the carrier of [:T,T:]:] is non empty set
RelStr(# the carrier of [:T,T:], the InternalRel of [:T,T:] #) is strict RelStr
y is Relation-like the carrier of x -defined the carrier of T -valued Function-like V18( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
bool the carrier of x is non empty set
x9 is Element of bool the carrier of x
bool the carrier of [:T,T:] is non empty set
y .: x9 is Element of bool the carrier of T
bool the carrier of T is non empty set
"/\" ((y .: x9),T) is Element of the carrier of T
"/\" (x9,x) is Element of the carrier of x
K76( the carrier of x, the carrier of T,y,("/\" (x9,x))) is Element of the carrier of T
y9 is Element of bool the carrier of [:T,T:]
"/\" (y9,[:T,T:]) is Element of the carrier of [:T,T:]
(inf_op T) . ("/\" (y9,[:T,T:])) is Element of the carrier of T
y . ("/\" (x9,x)) is Element of the carrier of T
F₁() is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima non void TopRelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
bool (bool the carrier of F₁()) is non empty set
[#] F₁() is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of F₁()
T is V69(F₁()) quasi_prebasis Element of bool (bool the carrier of F₁())
T is V69(F₁()) quasi_prebasis Element of bool (bool the carrier of F₁())
x is Element of bool the carrier of F₁()
the topology of F₁() is non empty Element of bool (bool the carrier of F₁())
FinMeetCl T is Element of bool (bool the carrier of F₁())
UniCl (FinMeetCl T) is Element of bool (bool the carrier of F₁())
y is Element of bool (bool the carrier of F₁())
union y is Element of bool the carrier of F₁()
y9 is Element of bool the carrier of F₁()
x9 is Element of bool (bool the carrier of F₁())
u is Element of bool (bool the carrier of F₁())
Intersect u is Element of bool the carrier of F₁()
W is set
V is set
{W} is non empty finite set
V \/ {W} is non empty set
x is Element of bool (bool the carrier of F₁())
z is Element of bool (bool the carrier of F₁())
Y is Element of bool (bool the carrier of F₁())
I2 is Element of bool (bool the carrier of F₁())
Z is Element of bool (bool the carrier of F₁())
Intersect Z is Element of bool the carrier of F₁()
y is Element of bool the carrier of F₁()
a is Element of bool (bool the carrier of F₁())
Intersect a is Element of bool the carrier of F₁()
Y is Element of bool (bool the carrier of F₁())
Intersect Y is Element of bool the carrier of F₁()
J2 is Element of bool the carrier of F₁()
J2 /\ y is Element of bool the carrier of F₁()
W is Element of bool (bool the carrier of F₁())
Intersect W is Element of bool the carrier of F₁()
T is non empty reflexive antisymmetric up-complete 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
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of x is non empty set
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
y is Element of the carrier of x
waybelow y is Element of bool the carrier of x
bool the carrier of x is non empty set
{ b₁ where b₁ is Element of the carrier of x : b₁ is_way_below y } is set
"\/" ((waybelow y),x) is Element of the carrier of x
x9 is Element of the carrier of T
waybelow x9 is Element of bool the carrier of T
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of the carrier of T : b₁ is_way_below x9 } is set
"\/" ((waybelow x9),T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void RelStr
x is non empty reflexive transitive antisymmetric non void TopAugmentation of T
the carrier of x is non empty set
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict 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
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
T is TopSpace-like TopStruct
x is TopSpace-like TopStruct
the topology of T is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of x is non empty Element of bool (bool the carrier of x)
the carrier of x is set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
y is TopSpace-like Refinement of T,x
the carrier of y is set
bool the carrier of y is non empty set
x9 is Element of bool the carrier of y
the topology of T \/ the topology of x is non empty set
bool (bool the carrier of y) is non empty set
the topology of y is non empty Element of bool (bool the carrier of y)
T is TopSpace-like TopStruct
x is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
y is TopSpace-like Refinement of T,x
the carrier of y is set
bool the carrier of y is non empty set
x9 is Element of bool the carrier of T
y9 is Element of bool the carrier of y
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
T is TopSpace-like TopStruct
the carrier of T is set
x is TopSpace-like TopStruct
the carrier of x is set
bool the carrier of T is non empty set
y is TopSpace-like Refinement of T,x
the carrier of y is set
bool the carrier of y is non empty set
x9 is Element of bool the carrier of T
y9 is Element of bool the carrier of y
x9 ` is Element of bool the carrier of T
the carrier of T \ x9 is set
the carrier of T \/ the carrier of x is set
y9 ` is Element of bool the carrier of y
the carrier of y \ y9 is set
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the topology of T is non empty Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is set
y is set
x9 is Element of bool (bool the carrier of T)
y9 is Element of bool (bool the carrier of T)
u is Element of bool (bool the carrier of T)
W is Element of bool (bool the carrier of T)
V is Element of bool (bool the carrier of T)
UniCl V is Element of bool (bool the carrier of T)
x is Element of bool (bool the carrier of T)
UniCl x is Element of bool (bool the carrier of T)
UniCl the topology of T is Element of bool (bool the carrier of T)
FinMeetCl the topology of T is Element of bool (bool the carrier of T)
FinMeetCl x is Element of bool (bool the carrier of T)
UniCl (FinMeetCl x) is Element of bool (bool the carrier of T)
FinMeetCl V is Element of bool (bool the carrier of T)
UniCl (FinMeetCl V) is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is non empty TopSpace-like TopStruct
the carrier of x is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
y is non empty TopSpace-like Refinement of T,x
the carrier of y is non empty set
bool the carrier of y is non empty set
bool (bool the carrier of y) is non empty set
x9 is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
y9 is V69(x) quasi_prebasis Element of bool (bool the carrier of x)
x9 \/ y9 is set
the carrier of T \/ the carrier of x is non empty set
{ the carrier of T, the carrier of x} is non empty finite set
{ the carrier of y} is non empty finite set
(x9 \/ y9) \/ { the carrier of y} is non empty set
u is V69(y) quasi_prebasis Element of bool (bool the carrier of y)
W is Element of bool (bool the carrier of y)
FinMeetCl W is Element of bool (bool the carrier of y)
V is set
FinMeetCl u is Element of bool (bool the carrier of y)
FinMeetCl (FinMeetCl W) is Element of bool (bool the carrier of y)
T is non empty TopSpace-like TopStruct
x is non empty TopSpace-like TopStruct
y is non empty TopSpace-like TopStruct
x9 is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the carrier of y is non empty set
[: the carrier of T, the carrier of y:] is non empty set
bool [: the carrier of T, the carrier of y:] is non empty set
the carrier of x is non empty set
the carrier of x9 is non empty set
[: the carrier of x, the carrier of x9:] is non empty set
bool [: the carrier of x, the carrier of x9:] is non empty set
y9 is non empty TopSpace-like Refinement of T,x
the carrier of y9 is non empty set
u is non empty TopSpace-like Refinement of y,x9
the carrier of u is non empty set
[: the carrier of y9, the carrier of u:] is non empty set
bool [: the carrier of y9, the carrier of u:] is non empty set
W is Relation-like the carrier of T -defined the carrier of y -valued Function-like V18( the carrier of T, the carrier of y) Element of bool [: the carrier of T, the carrier of y:]
V is Relation-like the carrier of x -defined the carrier of x9 -valued Function-like V18( the carrier of x, the carrier of x9) Element of bool [: the carrier of x, the carrier of x9:]
x is Relation-like the carrier of y9 -defined the carrier of u -valued Function-like V18( the carrier of y9, the carrier of u) Element of bool [: the carrier of y9, the carrier of u:]
[#] x9 is non empty non proper open closed dense non boundary Element of bool the carrier of x9
bool the carrier of x9 is non empty set
bool the carrier of u is non empty set
bool (bool the carrier of u) is non empty set
the topology of y is non empty Element of bool (bool the carrier of y)
bool the carrier of y is non empty set
bool (bool the carrier of y) is non empty set
the topology of x9 is non empty Element of bool (bool the carrier of x9)
bool (bool the carrier of x9) is non empty set
the topology of y \/ the topology of x9 is non empty set
[#] y is non empty non proper open closed dense non boundary Element of bool the carrier of y
Y is Element of bool the carrier of u
z is V69(u) quasi_prebasis Element of bool (bool the carrier of u)
I2 is Element of bool the carrier of y
W " I2 is Element of bool the carrier of T
bool the carrier of T is non empty set
x " Y is Element of bool the carrier of y9
bool the carrier of y9 is non empty set
I2 is Element of bool the carrier of x9
V " I2 is Element of bool the carrier of x
bool the carrier of x is non empty set
x " Y is Element of bool the carrier of y9
bool the carrier of y9 is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
y is non empty transitive directed NetStr over T
Lim y is Element of bool the carrier of T
x9 is Element of the carrier of T
the carrier of y is non empty set
y9 is a_neighborhood of x9
Int y9 is open Element of bool the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
FinMeetCl x is Element of bool (bool the carrier of T)
UniCl (FinMeetCl x) is Element of bool (bool the carrier of T)
u is Element of bool (bool the carrier of T)
union u is Element of bool the carrier of T
W is set
V is Element of bool (bool the carrier of T)
Intersect V is Element of bool the carrier of T
x is set
z is Element of bool the carrier of T
Y is Element of the carrier of y
I2 is Element of the carrier of y
Y is Element of the carrier of y
y . Y is Element of the carrier of T
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V18( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty set
bool [: the carrier of y, the carrier of T:] is non empty set
K76( the carrier of y, the carrier of T, the mapping of y,Y) is Element of the carrier of T
x is Relation-like Function-like set
dom x is set
rng x is set
[#] y is non empty non proper lower upper Element of bool the carrier of y
bool the carrier of y is non empty set
bool ([#] y) is non empty set
z is finite Element of bool ([#] y)
Y is Element of the carrier of y
I2 is Element of the carrier of y
y . I2 is Element of the carrier of T
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V18( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty set
bool [: the carrier of y, the carrier of T:] is non empty set
K76( the carrier of y, the carrier of T, the mapping of y,I2) is Element of the carrier of T
Y is set
x . Y is set
Z is Element of the carrier of y
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty transitive directed NetStr over T
Lim x is Element of bool the carrier of T
y is Element of bool the carrier of T
Cl y is closed Element of bool the carrier of T
the carrier of x is non empty set
x9 is Element of the carrier of x
y9 is set
u is Element of the carrier of T
W is a_neighborhood of u
V is Element of the carrier of x
[#] x is non empty non proper lower upper Element of bool the carrier of x
bool the carrier of x is non empty set
x is Element of the carrier of x
x . x is Element of the carrier of T
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V18( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
[: the carrier of x, the carrier of T:] is non empty set
bool [: the carrier of x, the carrier of T:] is non empty set
K76( the carrier of x, the carrier of T, the mapping of x,x) is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty Element of bool the carrier of T
x +id is non empty strict NetStr over T
subrelstr x is strict full SubRelStr of T
K448(T,(subrelstr x)) is Relation-like the carrier of (subrelstr x) -defined the carrier of T -valued Function-like V18( the carrier of (subrelstr x), the carrier of T) Element of bool [: the carrier of (subrelstr x), the carrier of T:]
the carrier of (subrelstr x) is set
[: the carrier of (subrelstr x), the carrier of T:] is set
bool [: the carrier of (subrelstr x), the carrier of T:] is non empty set
(subrelstr x) +id is strict NetStr over subrelstr x
K448(T,(subrelstr x)) * ((subrelstr x) +id) is strict NetStr over T
the mapping of (x +id) is non empty Relation-like the carrier of (x +id) -defined the carrier of T -valued Function-like V18( the carrier of (x +id), the carrier of T) Element of bool [: the carrier of (x +id), the carrier of T:]
the carrier of (x +id) is non empty set
[: the carrier of (x +id), the carrier of T:] is non empty set
bool [: the carrier of (x +id), the carrier of T:] is non empty set
id x is non empty Relation-like set
x opp+id is non empty strict NetStr over T
(subrelstr x) opp+id is strict NetStr over subrelstr x
K448(T,(subrelstr x)) * ((subrelstr x) opp+id) is strict NetStr over T
the mapping of (x opp+id) is non empty Relation-like the carrier of (x opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (x opp+id), the carrier of T) Element of bool [: the carrier of (x opp+id), the carrier of T:]
the carrier of (x opp+id) is non empty set
[: the carrier of (x opp+id), the carrier of T:] is non empty set
bool [: the carrier of (x opp+id), the carrier of T:] is non empty set
y is set
the mapping of (x +id) . y is set
x9 is Element of the carrier of (x +id)
(x +id) . x9 is Element of the carrier of T
K76( the carrier of (x +id), the carrier of T, the mapping of (x +id),x9) is Element of the carrier of T
dom the mapping of (x +id) is Element of bool the carrier of (x +id)
bool the carrier of (x +id) is non empty set
y is set
the mapping of (x opp+id) . y is set
x9 is Element of the carrier of (x opp+id)
(x opp+id) . x9 is Element of the carrier of T
K76( the carrier of (x opp+id), the carrier of T, the mapping of (x opp+id),x9) is Element of the carrier of T
dom the mapping of (x opp+id) is Element of bool the carrier of (x opp+id)
bool the carrier of (x opp+id) is non empty set
T is non empty reflexive antisymmetric non void RelStr
the carrier of T is non empty set
x is Element of the carrier of T
uparrow x is non empty filtered Element of bool the carrier of T
bool the carrier of T is non empty set
{x} is non empty finite Element of bool the carrier of T
uparrow {x} is non empty Element of bool the carrier of T
downarrow x is non empty directed Element of bool the carrier of T
downarrow {x} is non empty Element of bool the carrier of T
(uparrow x) /\ (downarrow x) is Element of bool the carrier of T
y is set
x9 is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
x is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
y is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
x9 is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void TopAugmentation of T
the topology of y is non empty Element of bool (bool the carrier of y)
the carrier of y is non empty set
bool the carrier of y is non empty set
bool (bool the carrier of y) is non empty set
sigma T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
the carrier of T \/ the carrier of T is non empty set
the topology of x is non empty Element of bool (bool the carrier of x)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
(T) is Element of bool (bool the carrier of T)
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of x9 is non empty set
bool the carrier of x9 is non empty set
(x9) is Element of bool (bool the carrier of x9)
bool (bool the carrier of x9) is non empty set
sigma x9 is Element of bool (bool the carrier of x9)
Scott-Convergence x9 is Relation-like V237(x9) V238(x9) M36(x9)
K436(x9,(Scott-Convergence x9)) is non empty strict TopSpace-like TopStruct
the topology of K436(x9,(Scott-Convergence x9)) is non empty Element of bool (bool the carrier of K436(x9,(Scott-Convergence x9)))
the carrier of K436(x9,(Scott-Convergence x9)) is non empty set
bool the carrier of K436(x9,(Scott-Convergence x9)) is non empty set
bool (bool the carrier of K436(x9,(Scott-Convergence x9))) is non empty set
(x9) \/ (sigma x9) is Element of bool (bool the carrier of x9)
the InternalRel of y is non empty Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the InternalRel of x9 is non empty Relation-like the carrier of x9 -defined the carrier of x9 -valued Element of bool [: the carrier of x9, the carrier of x9:]
[: the carrier of x9, the carrier of x9:] is non empty set
bool [: the carrier of x9, the carrier of x9:] is non empty set
RelStr(# the carrier of x9, the InternalRel of x9 #) is strict RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict 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
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T \/ the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
y9 is Element of bool (bool the carrier of T)
TopRelStr(# the carrier of T, the InternalRel of T,y9 #) is strict TopRelStr
the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #) is set
the InternalRel of TopRelStr(# the carrier of T, the InternalRel of T,y9 #) is Relation-like the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #) -defined the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #):]
[: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #):] is set
bool [: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of T, the InternalRel of T,y9 #), the InternalRel of TopRelStr(# the carrier of T, the InternalRel of T,y9 #) #) is strict RelStr
W is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void TopAugmentation of T
the carrier of W is non empty set
the topology of W is Element of bool (bool the carrier of W)
bool the carrier of W is non empty set
bool (bool the carrier of W) is non empty set
TopStruct(# the carrier of W, the topology of W #) is non empty strict TopStruct
TopStruct(# the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the topology of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is non empty strict TopSpace-like TopStruct
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T \/ the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
V is V69( the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
FinMeetCl V is Element of bool (bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
UniCl (FinMeetCl V) is Element of bool (bool the carrier of the non empty TopSpace-like Refinement of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
x is Element of bool (bool the carrier of W)
FinMeetCl x is Element of bool (bool the carrier of W)
the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete strict Scott non void TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete strict Scott non void TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void RelStr is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void RelStr
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete strict non void () TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void RelStr is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete strict non void () TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void RelStr
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
sigma T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
(sigma T) \/ { ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T : verum } is set
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
u is set
W is Element of the carrier of T
uparrow W is non empty filtered upper Element of bool the carrier of T
{W} is non empty finite compact Element of bool the carrier of T
uparrow {W} is non empty upper Element of bool the carrier of T
(uparrow W) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow W) is set
V is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow V is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
{V} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow {V} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
u is set
W is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow W is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
{W} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow {W} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow W) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T \ (uparrow W) is set
V is Element of the carrier of T
uparrow V is non empty filtered upper Element of bool the carrier of T
{V} is non empty finite compact Element of bool the carrier of T
uparrow {V} is non empty upper Element of bool the carrier of T
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
u is V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
sigma T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
{ (b<sub>1</sub> \ (uparrow b<sub>2</sub>)) where b<sub>1</sub> is Element of bool the carrier of T, b<sub>2</sub> is Element of the carrier of T : b<sub>1</sub> in sigma T } is set
(sigma T) \/ { (b<sub>1</sub> \ (uparrow b<sub>2</sub>)) where b<sub>1</sub> is Element of bool the carrier of T, b<sub>2</sub> is Element of the carrier of T : b<sub>1</sub> in sigma T } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T : verum } is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
y9 is set
u is Element of bool the carrier of T
W is Element of the carrier of T
uparrow W is non empty filtered upper Element of bool the carrier of T
{W} is non empty finite compact Element of bool the carrier of T
uparrow {W} is non empty upper Element of bool the carrier of T
u \ (uparrow W) is Element of bool the carrier of T
y9 is Element of bool (bool the carrier of T)
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
(T) is Element of bool (bool the carrier of T)
(sigma T) \/ (T) is Element of bool (bool the carrier of T)
the topology of T is non empty Element of bool (bool the carrier of T)
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
u is Element of bool (bool the carrier of T)
V is set
x is Element of bool the carrier of T
z is Element of the carrier of T
uparrow z is non empty filtered upper Element of bool the carrier of T
{z} is non empty finite compact Element of bool the carrier of T
uparrow {z} is non empty upper Element of bool the carrier of T
x \ (uparrow z) is Element of bool the carrier of T
(uparrow z) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow z) is set
x /\ ((uparrow z) `) is Element of bool the carrier of T
Y is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow Y is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
{Y} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow {Y} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
y is V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
(sigma T) \/ u is Element of bool (bool the carrier of T)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
y is V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
V is set
x is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow x is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
{x} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow {x} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow x) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T \ (uparrow x) is set
[#] T 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 T
z is Element of the carrier of T
uparrow z is non empty filtered upper Element of bool the carrier of T
{z} is non empty finite compact Element of bool the carrier of T
uparrow {z} is non empty upper Element of bool the carrier of T
([#] T) \ (uparrow z) is Element of bool the carrier of T
(sigma T) \/ y is set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
sigma T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
{ (b<sub>1</sub> \ (uparrow b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of T : ( b<sub>1</sub> in sigma T & b<sub>2</sub> is finite ) } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T : b₁ is finite } is set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
u is non empty V69( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
{} the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
x is set
V is Element of bool the carrier of T
uparrow V is upper Element of bool the carrier of T
uparrow ({} the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
z is Element of bool the carrier of T
z \ (uparrow V) is Element of bool the carrier of T
u \/ { (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of bool the carrier of T : ( b₁ in sigma T & b₂ is finite ) } is non empty set
y is non empty V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) quasi_basis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
INTERSECTION (u,y) is set
W is set
V is set
x is set
V /\ x is set
[#] T 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 T
z is Element of bool the carrier of T
([#] T) /\ z is Element of bool the carrier of T
Y is Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow Y is upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow Y) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T \ (uparrow Y) is set
I2 is Element of bool the carrier of T
uparrow I2 is upper Element of bool the carrier of T
(uparrow I2) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow I2) is set
z \ (uparrow I2) is Element of bool the carrier of T
W is set
V is Element of bool the carrier of T
x is Element of bool the carrier of T
uparrow x is upper Element of bool the carrier of T
V \ (uparrow x) is Element of bool the carrier of T
V /\ ([#] T) is Element of bool the carrier of T
([#] T) \ (uparrow x) is Element of bool the carrier of T
V /\ (([#] T) \ (uparrow x)) is Element of bool the carrier of T
z is Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow z is upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow z) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T \ (uparrow z) is set
(uparrow x) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow x) is set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
W is set
V is Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow V is upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow V) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T \ (uparrow V) is set
x is Element of bool the carrier of T
uparrow x is upper Element of bool the carrier of T
y \/ { (b<sub>1</sub> \ (uparrow b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of T : ( b<sub>1</sub> in sigma T & b<sub>2</sub> is finite ) } is non empty set
u \/ y is non empty set
(u \/ y) \/ (INTERSECTION (u,y)) is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
y is Element of bool (bool the carrier of T)
x9 is Element of bool (bool the carrier of T)
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
y is Element of bool (bool the carrier of T)
x9 is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the topology of x9 is non empty Element of bool (bool the carrier of x9)
the carrier of x9 is non empty set
bool the carrier of x9 is non empty set
bool (bool the carrier of x9) is non empty set
the InternalRel of x9 is non empty Relation-like the carrier of x9 -defined the carrier of x9 -valued Element of bool [: the carrier of x9, the carrier of x9:]
[: the carrier of x9, the carrier of x9:] is non empty set
bool [: the carrier of x9, the carrier of x9:] is non empty set
RelStr(# the carrier of x9, the InternalRel of x9 #) is strict RelStr
sigma x9 is Element of bool (bool the carrier of x9)
Scott-Convergence x9 is Relation-like V237(x9) V238(x9) M36(x9)
K436(x9,(Scott-Convergence x9)) is non empty strict TopSpace-like TopStruct
the topology of K436(x9,(Scott-Convergence x9)) is non empty Element of bool (bool the carrier of K436(x9,(Scott-Convergence x9)))
the carrier of K436(x9,(Scott-Convergence x9)) is non empty set
bool the carrier of K436(x9,(Scott-Convergence x9)) is non empty set
bool (bool the carrier of K436(x9,(Scott-Convergence x9))) is non empty set
sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is Relation-like V237( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) V238( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) M36( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty strict TopSpace-like TopStruct
the topology of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty Element of bool (bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)))
the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty set
bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty set
bool (bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T))) is non empty set
(x9) is Element of bool (bool the carrier of x9)
(x9) \/ (sigma x9) is Element of bool (bool the carrier of x9)
FinMeetCl ((x9) \/ (sigma x9)) is Element of bool (bool the carrier of x9)
( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
FinMeetCl (( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
UniCl (FinMeetCl (( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T))) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
(T) is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
sigma T is Element of bool (bool the carrier of T)
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
(T) is Element of bool (bool the carrier of T)
(sigma T) \/ (T) is Element of bool (bool the carrier of T)
FinMeetCl ((sigma T) \/ (T)) is Element of bool (bool the carrier of T)
UniCl (FinMeetCl ((sigma T) \/ (T))) is Element of bool (bool the carrier of T)
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is Relation-like V237( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) V238( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) M36( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty strict TopSpace-like TopStruct
the topology of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty Element of bool (bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)))
the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty set
bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is non empty set
bool (bool the carrier of K436( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T,(Scott-Convergence the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T))) is non empty set
( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
FinMeetCl (( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
UniCl (FinMeetCl (( the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) \/ (sigma the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T))) is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
(T) is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
y is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
x9 is non empty TopSpace-like Refinement of y,x
the topology of x9 is non empty Element of bool (bool the carrier of x9)
the carrier of x9 is non empty set
bool the carrier of x9 is non empty set
bool (bool the carrier of x9) is non empty set
the carrier of x is non empty set
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of T \/ the carrier of T is non empty set
the carrier of y is non empty set
the InternalRel of y is non empty Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
sigma T is Element of bool (bool the carrier of T)
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
the topology of y is non empty Element of bool (bool the carrier of y)
bool the carrier of y is non empty set
bool (bool the carrier of y) is non empty set
(T) is Element of bool (bool the carrier of T)
the topology of x is non empty Element of bool (bool the carrier of x)
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
(sigma T) \/ (T) is Element of bool (bool the carrier of T)
FinMeetCl ((sigma T) \/ (T)) is Element of bool (bool the carrier of T)
UniCl (FinMeetCl ((sigma T) \/ (T))) is Element of bool (bool the carrier of T)
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is Element of bool (bool the carrier of T)
union x is Element of bool the carrier of T
y is non empty directed Element of bool the carrier of T
"\/" (y,T) is Element of the carrier of T
x9 is set
y9 is Element of bool the carrier of T
u is Element of the carrier of T
W is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is Element of bool the carrier of T
y is Element of bool the carrier of T
x /\ y is Element of bool the carrier of T
x9 is non empty directed Element of bool the carrier of T
"\/" (x9,T) is Element of the carrier of T
y9 is Element of the carrier of T
u is Element of the carrier of T
W is Element of the carrier of T
V is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[#] T is non empty non proper directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty directed Element of bool the carrier of T
"\/" (x,T) is Element of the carrier of T
the Element of x is Element of x
x9 is Element of the carrier of T
y9 is Element of the carrier of T
T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
y is Element of bool the carrier of T
x9 is Element of the carrier of T
uparrow x9 is non empty filtered upper Element of bool the carrier of T
{x9} is non empty finite compact Element of bool the carrier of T
uparrow {x9} is non empty upper Element of bool the carrier of T
(uparrow x9) ` is lower Element of bool the carrier of T
the carrier of T \ (uparrow x9) is set
y9 is non empty directed Element of bool the carrier of T
"\/" (y9,T) is Element of the carrier of T
the Element of y9 is Element of y9
W is Element of the carrier of T
V is Element of the carrier of T
{V} is non empty finite compact Element of bool the carrier of T
"\/" ({V},T) is Element of the carrier of T
x is Element of bool the carrier of T
y is Element of bool the carrier of T
x /\ y is Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of T
x is Element of bool (bool the carrier of T)
union x is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
bool (bool the carrier of T) is non empty set
sigma T is Element of bool (bool the carrier of T)
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
(T) is Element of bool (bool the carrier of T)
(sigma T) \/ (T) is Element of bool (bool the carrier of T)
x9 is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
y9 is Element of bool the carrier of T
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T)
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T) is non empty set
u is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
W is Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
[#] T 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 T
x9 is Element of bool the carrier of T
y9 is Element of bool the carrier of T
x9 /\ y9 is Element of bool the carrier of T
x9 is Element of bool (bool the carrier of T)
union x9 is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of x is non empty set
bool the carrier of x is non empty set
y is Element of bool the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
x9 is Element of bool the carrier of x
sigma x is Element of bool (bool the carrier of x)
bool (bool the carrier of x) is non empty set
Scott-Convergence x is Relation-like V237(x) V238(x) M36(x)
K436(x,(Scott-Convergence x)) is non empty strict TopSpace-like TopStruct
the topology of K436(x,(Scott-Convergence x)) is non empty Element of bool (bool the carrier of K436(x,(Scott-Convergence x)))
the carrier of K436(x,(Scott-Convergence x)) is non empty set
bool the carrier of K436(x,(Scott-Convergence x)) is non empty set
bool (bool the carrier of K436(x,(Scott-Convergence x))) is non empty set
(x) is Element of bool (bool the carrier of x)
(sigma x) \/ (x) is Element of bool (bool the carrier of x)
the topology of x is non empty Element of bool (bool the carrier of x)
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
x9 is Element of the carrier of T
uparrow x9 is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{x9} is non empty finite compact Element of bool the carrier of T
uparrow {x9} is non empty upper Element of bool the carrier of T
downarrow x9 is non empty directed lower property(S) Element of bool the carrier of T
downarrow {x9} is non empty lower property(S) Element of bool the carrier of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
y9 is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
downarrow y9 is non empty directed lower property(S) Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
{y9} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
downarrow {y9} is non empty lower property(S) Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T #) is strict RelStr
u is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow u is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T is non empty set
{u} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
uparrow {u} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
(uparrow x9) /\ (downarrow x9) is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
uparrow x is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{x} is non empty finite compact Element of bool the carrier of T
uparrow {x} is non empty upper Element of bool the carrier of T
(uparrow x) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow x) is set
downarrow x is non empty directed lower property(S) Element of bool the carrier of T
downarrow {x} is non empty lower property(S) Element of bool the carrier of T
(downarrow x) ` is upper closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ (downarrow x) is set
{x} ` is Element of bool the carrier of T
the carrier of T \ {x} is set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
wayabove x is upper Element of bool the carrier of T
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of the carrier of T : x is_way_below b₁ } is set
(wayabove x) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (wayabove x) is set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x9 is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T
wayabove x9 is upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete Scott non void TopAugmentation of T : x9 is_way_below b<sub>1</sub> } is set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopAugmentation of T
the carrier of x is non empty set
bool the carrier of x is non empty set
y is upper Element of bool the carrier of x
x9 is Element of bool the carrier of T
the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
x is lower property(S) Element of bool the carrier of T
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
x ` is upper closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ x is set
x9 is property(S) Element of bool the carrier of T
x9 ` is closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ x9 is set
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
x9 is lower closed_under_directed_sups property(S) Element of bool the carrier of T
x9 ` is upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ x9 is set
y9 is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
sigma T is Element of bool (bool the carrier of T)
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
(sigma T) \/ { ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
x9 is non empty filtered Element of bool the carrier of T
x9 opp+id is non empty reflexive transitive strict directed non void NetStr over T
subrelstr x9 is strict reflexive transitive antisymmetric full SubRelStr of T
K448(T,(subrelstr x9)) is Relation-like the carrier of (subrelstr x9) -defined the carrier of T -valued Function-like V18( the carrier of (subrelstr x9), the carrier of T) Element of bool [: the carrier of (subrelstr x9), the carrier of T:]
the carrier of (subrelstr x9) is set
[: the carrier of (subrelstr x9), the carrier of T:] is set
bool [: the carrier of (subrelstr x9), the carrier of T:] is non empty set
(subrelstr x9) opp+id is strict strict directed NetStr over subrelstr x9
K448(T,(subrelstr x9)) * ((subrelstr x9) opp+id) is strict NetStr over T
Lim (x9 opp+id) is Element of bool the carrier of T
"/\" (x9,T) is Element of the carrier of T
{("/\" (x9,T))} is non empty finite compact Element of bool the carrier of T
the carrier of (x9 opp+id) is non empty set
T ~ is non empty strict reflexive transitive antisymmetric non void RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
u is set
the mapping of (x9 opp+id) is non empty Relation-like the carrier of (x9 opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (x9 opp+id), the carrier of T) Element of bool [: the carrier of (x9 opp+id), the carrier of T:]
[: the carrier of (x9 opp+id), the carrier of T:] is non empty set
bool [: the carrier of (x9 opp+id), the carrier of T:] is non empty set
id x9 is non empty Relation-like set
rng the mapping of (x9 opp+id) is Element of bool the carrier of T
W is Element of the carrier of T
Cl x9 is closed Element of bool the carrier of T
V is Element of the carrier of T
downarrow V is non empty directed lower property(S) Element of bool the carrier of T
{V} is non empty finite compact Element of bool the carrier of T
downarrow {V} is non empty lower property(S) Element of bool the carrier of T
x is Element of the carrier of (x9 opp+id)
z is Element of the carrier of (x9 opp+id)
(x9 opp+id) . z is Element of the carrier of T
K76( the carrier of (x9 opp+id), the carrier of T, the mapping of (x9 opp+id),z) is Element of the carrier of T
V ~ is Element of the carrier of (T ~)
the carrier of (T ~) is non empty set
Y is Element of the carrier of T
Y ~ is Element of the carrier of (T ~)
Cl (downarrow V) is closed Element of bool the carrier of T
uparrow ("/\" (x9,T)) is non empty filtered upper Element of bool the carrier of T
uparrow {("/\" (x9,T))} is non empty upper Element of bool the carrier of T
Cl (uparrow ("/\" (x9,T))) is closed Element of bool the carrier of T
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
u is Element of bool the carrier of T
x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
the Element of the carrier of (x9 opp+id) is Element of the carrier of (x9 opp+id)
W is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
x is Element of the carrier of (x9 opp+id)
(x9 opp+id) . x is Element of the carrier of T
the mapping of (x9 opp+id) is non empty Relation-like the carrier of (x9 opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (x9 opp+id), the carrier of T) Element of bool [: the carrier of (x9 opp+id), the carrier of T:]
[: the carrier of (x9 opp+id), the carrier of T:] is non empty set
bool [: the carrier of (x9 opp+id), the carrier of T:] is non empty set
K76( the carrier of (x9 opp+id), the carrier of T, the mapping of (x9 opp+id),x) is Element of the carrier of T
z is Element of the carrier of T
W is Element of the carrier of T
uparrow W is non empty filtered upper Element of bool the carrier of T
{W} is non empty finite compact Element of bool the carrier of T
uparrow {W} is non empty upper Element of bool the carrier of T
(uparrow W) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow W) is set
V is Element of the carrier of T
x is Element of the carrier of (x9 opp+id)
z is Element of the carrier of (x9 opp+id)
(x9 opp+id) . z is Element of the carrier of T
the mapping of (x9 opp+id) is non empty Relation-like the carrier of (x9 opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (x9 opp+id), the carrier of T) Element of bool [: the carrier of (x9 opp+id), the carrier of T:]
[: the carrier of (x9 opp+id), the carrier of T:] is non empty set
bool [: the carrier of (x9 opp+id), the carrier of T:] is non empty set
K76( the carrier of (x9 opp+id), the carrier of T, the mapping of (x9 opp+id),z) is Element of the carrier of T
V ~ is Element of the carrier of (T ~)
the carrier of (T ~) is non empty set
Y is Element of the carrier of T
Y ~ is Element of the carrier of (T ~)
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite compact Element of bool the carrier of T
bool the carrier of T is non empty set
sigma T is 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
Scott-Convergence T is Relation-like V237(T) V238(T) M36(T)
K436(T,(Scott-Convergence T)) is non empty strict TopSpace-like TopStruct
the topology of K436(T,(Scott-Convergence T)) is non empty Element of bool (bool the carrier of K436(T,(Scott-Convergence T)))
the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool the carrier of K436(T,(Scott-Convergence T)) is non empty set
bool (bool the carrier of K436(T,(Scott-Convergence T))) is non empty set
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
(sigma T) \/ { ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the topology of T is non empty Element of bool (bool the carrier of T)
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T #) is strict RelStr
the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x9 is V69(T) quasi_prebasis Element of bool (bool the carrier of T)
bool x9 is non empty set
u is Element of the carrier of (InclPoset the topology of T)
W is Element of bool x9
union W is set
bool W is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of T : (uparrow b<sub>1</sub>) ` in W } is set
"\/" ( { b₁ where b₁ is Element of the carrier of T : (uparrow b₁) ` in W } ,T) is Element of the carrier of T
z is set
Y is Element of the carrier of T
uparrow Y is non empty filtered upper Element of bool the carrier of T
{Y} is non empty finite compact Element of bool the carrier of T
uparrow {Y} is non empty upper Element of bool the carrier of T
(uparrow Y) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow Y) is set
Y is set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty set
Y is Element of bool the carrier of T
I2 is Element of bool the carrier of T
y is Element of the carrier of T
uparrow y is non empty filtered upper Element of bool the carrier of T
{y} is non empty finite compact Element of bool the carrier of T
uparrow {y} is non empty upper Element of bool the carrier of T
(uparrow y) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow y) is set
Z is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the topology of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is non empty set
z is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
J2 is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
"\/" (J2, the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
finsups J2 is non empty directed Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
bool J2 is non empty set
{ ("\/" (b<sub>1</sub>, the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T)) where b<sub>1</sub> is finite Element of bool J2 : ex_sup_of b<sub>1</sub>, the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T } is set
"\/" ((finsups J2), the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
y is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
a is finite Element of bool J2
"\/" (a, the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
{ ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : b₁ in a } is set
{Y} is non empty finite Element of bool (bool the carrier of T)
{Y} \/ { ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : b<sub>1</sub> in a } is non empty set
G is set
u is Element of the carrier of T
uparrow u is non empty filtered upper Element of bool the carrier of T
{u} is non empty finite compact Element of bool the carrier of T
uparrow {u} is non empty upper Element of bool the carrier of T
(uparrow u) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow u) is set
u is Element of the carrier of T
uparrow u is non empty filtered upper Element of bool the carrier of T
{u} is non empty finite compact Element of bool the carrier of T
uparrow {u} is non empty upper Element of bool the carrier of T
(uparrow u) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow u) is set
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of T : b<sub>1</sub> in a } is set
G is finite Element of bool W
union G is set
u is set
union {Y} is Element of bool the carrier of T
union { ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : b₁ in a } is set
(union {Y}) \/ (union { ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : b<sub>1</sub> in a } ) is set
Y \/ (union { ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : b₁ in a } ) is set
u is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
v is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
c is Element of the carrier of T
uparrow c is non empty filtered upper Element of bool the carrier of T
{c} is non empty finite compact Element of bool the carrier of T
uparrow {c} is non empty upper Element of bool the carrier of T
(uparrow c) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow c) is set
uparrow v is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
{v} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
uparrow {v} is non empty upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
(uparrow v) ` is lower property(S) Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete Scott non void TopAugmentation of T \ (uparrow v) is set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous up-complete /\-complete non void TopRelStr
the carrier of T is non empty set
x is Element of the carrier of T
y is Element of the carrier of T
bool the carrier of T is non empty set
u is Element of the carrier of T
waybelow u is non empty directed lower property(S) Element of bool the carrier of T
{ b₁ where b₁ is Element of the carrier of T : b₁ is_way_below u } is set
W is Element of the carrier of T
waybelow W is non empty directed lower property(S) Element of bool the carrier of T
{ b₁ where b₁ is Element of the carrier of T : b₁ is_way_below W } is set
y9 is Element of the carrier of T
x9 is Element of the carrier of T
u is Element of the carrier of T
uparrow u is non empty filtered upper Element of bool the carrier of T
{u} is non empty finite compact Element of bool the carrier of T
uparrow {u} is non empty upper Element of bool the carrier of T
(uparrow u) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow u) is set
W is lower property(S) Element of bool the carrier of T
wayabove u is upper Element of bool the carrier of T
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of T : u is_way_below b<sub>1</sub> } is set
V is upper Element of bool the carrier of T
W ` is upper closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ W is set
x9 is Element of the carrier of T
y9 is Element of the carrier of T
u is Element of the carrier of T
wayabove u is upper Element of bool the carrier of T
{ b₁ where b₁ is Element of the carrier of T : u is_way_below b₁ } is set
W is upper Element of bool the carrier of T
uparrow u is non empty filtered upper Element of bool the carrier of T
{u} is non empty finite compact Element of bool the carrier of T
uparrow {u} is non empty upper Element of bool the carrier of T
(uparrow u) ` is lower property(S) Element of bool the carrier of T
the carrier of T \ (uparrow u) is set
V is lower property(S) Element of bool the carrier of T
V ` is upper closed_under_directed_sups Element of bool the carrier of T
the carrier of T \ V is set
y9 is Element of the carrier of T
x9 is Element of the carrier of T