K42() is set
K46() is non empty non trivial V11() V12() V13() non finite cardinal limit_cardinal Element of bool K42()
bool K42() is non empty set
K41() is non empty non trivial V11() V12() V13() non finite cardinal limit_cardinal set
bool K41() is non empty non trivial non finite set
K215() is non empty strict TopSpace-like TopStruct
the carrier of K215() is non empty set
1 is non empty V11() V12() V13() V17() V18() finite cardinal Element of K46()
[:1,1:] is non empty finite set
bool [:1,1:] is non empty finite V43() set
[:[:1,1:],1:] is non empty finite set
bool [:[:1,1:],1:] is non empty finite V43() set
bool K46() is non empty non trivial non finite set
{} is empty V11() V12() V13() V15() V16() V17() V18() finite V43() cardinal {} -element set
the empty V11() V12() V13() V15() V16() V17() V18() finite V43() cardinal {} -element set is empty V11() V12() V13() V15() V16() V17() V18() finite V43() cardinal {} -element set
L is set
bool L is non empty set
bool (bool L) is non empty set
B is V11() V12() V13() V17() V18() finite cardinal set
B + 1 is V11() V12() V13() V17() V18() finite cardinal Element of K46()
x is finite Element of bool (bool L)
card x is V11() V12() V13() V17() V18() finite cardinal Element of K41()
union x is Element of bool L
y is Element of bool L
{y} is non empty trivial finite 1 -element Element of bool (bool L)
x \ {y} is finite Element of bool (bool L)
union (x \ {y}) is Element of bool L
y is Element of bool L
{y} is non empty trivial finite 1 -element Element of bool (bool L)
x \ {y} is finite Element of bool (bool L)
union (x \ {y}) is Element of bool L
cx is finite Element of bool (bool L)
cx \/ {y} is non empty finite Element of bool (bool L)
union cx is Element of bool L
dx is set
dy is set
card (cx \/ {y}) is non empty V11() V12() V13() V17() V18() finite cardinal Element of K41()
card cx is V11() V12() V13() V17() V18() finite cardinal Element of K41()
(card cx) + 1 is V11() V12() V13() V17() V18() finite cardinal Element of K46()
dx is finite Element of bool (bool L)
union dx is Element of bool L
dy is Element of bool L
{dy} is non empty trivial finite 1 -element Element of bool (bool L)
dx \ {dy} is finite Element of bool (bool L)
union (dx \ {dy}) is Element of bool L
y is finite Element of bool (bool L)
union y is Element of bool L
cx is Element of bool L
{cx} is non empty trivial finite 1 -element Element of bool (bool L)
y \ {cx} is finite Element of bool (bool L)
union (y \ {cx}) is Element of bool L
y is Element of bool L
{y} is non empty trivial finite 1 -element Element of bool (bool L)
x \ {y} is finite Element of bool (bool L)
union (x \ {y}) is Element of bool L
B is finite Element of bool (bool L)
union B is Element of bool L
card B is V11() V12() V13() V17() V18() finite cardinal Element of K41()
x is finite Element of bool (bool L)
card x is V11() V12() V13() V17() V18() finite cardinal Element of K41()
union x is Element of bool L
y is finite Element of bool (bool L)
union y is Element of bool L
cx is Element of bool L
{cx} is non empty trivial finite 1 -element Element of bool (bool L)
y \ {cx} is finite Element of bool (bool L)
union (y \ {cx}) is Element of bool L
L is 1-sorted
the carrier of L is set
bool the carrier of L is non empty set
B is Element of bool the carrier of L
x is Element of bool the carrier of L
x ` is Element of bool the carrier of L
the carrier of L \ x is set
B ` is Element of bool the carrier of L
the carrier of L \ B is set
(x `) ` is Element of bool the carrier of L
the carrier of L \ (x `) is set
L is 1-sorted
the carrier of L is set
bool the carrier of L is non empty set
B is Element of bool the carrier of L
B ` is Element of bool the carrier of L
the carrier of L \ B is set
[#] the carrier of L is non proper Element of bool the carrier of L
([#] the carrier of L) ` is Element of bool the carrier of L
the carrier of L \ ([#] the carrier of L) is set
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
B is Element of the carrier of L
x is Element of the carrier of L
B "/\" x is Element of the carrier of L
downarrow (B "/\" x) is lower Element of bool the carrier of L
bool the carrier of L is non empty set
{(B "/\" x)} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {(B "/\" x)} is lower Element of bool the carrier of L
downarrow B is lower Element of bool the carrier of L
{B} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {B} is lower Element of bool the carrier of L
downarrow x is lower Element of bool the carrier of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
(downarrow B) /\ (downarrow x) is Element of bool the carrier of L
y is set
cx is Element of the carrier of L
cx is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
B is Element of the carrier of L
x is Element of the carrier of L
B "\/" x is Element of the carrier of L
uparrow (B "\/" x) is upper Element of bool the carrier of L
bool the carrier of L is non empty set
{(B "\/" x)} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {(B "\/" x)} is upper Element of bool the carrier of L
uparrow B is upper Element of bool the carrier of L
{B} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {B} is upper Element of bool the carrier of L
uparrow x is upper Element of bool the carrier of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {x} is upper Element of bool the carrier of L
(uparrow B) /\ (uparrow x) is Element of bool the carrier of L
y is set
cx is Element of the carrier of L
cx is Element of the carrier of L
L is non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is lower Element of bool the carrier of L
"\/" (B,L) is Element of the carrier of L
downarrow ("\/" (B,L)) is Element of bool the carrier of L
{("\/" (B,L))} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {("\/" (B,L))} is Element of bool the carrier of L
L is non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is upper Element of bool the carrier of L
"/\" (B,L) is Element of the carrier of L
uparrow ("/\" (B,L)) is Element of bool the carrier of L
{("/\" (B,L))} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {("/\" (B,L))} is Element of bool the carrier of L
L is non empty reflexive transitive RelStr
the carrier of L is non empty set
B is Element of the carrier of L
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of bool the carrier of L
bool the carrier of L is non empty set
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {x} is non empty upper Element of bool the carrier of L
wayabove B is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : B is_way_below b1 } is set
y is set
cx is Element of the carrier of L
L is non empty reflexive transitive RelStr
the carrier of L is non empty set
B is Element of the carrier of L
x is Element of the carrier of L
downarrow B is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{B} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {B} is non empty lower Element of bool the carrier of L
waybelow x is lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below x } is set
y is set
cx is Element of the carrier of L
L is non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
B is Element of the carrier of L
waybelow B is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
"\/" ((waybelow B),L) is Element of the carrier of L
wayabove B is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : B is_way_below b1 } is set
"/\" ((wayabove B),L) is Element of the carrier of L
L is non empty antisymmetric lower-bounded RelStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
uparrow (Bottom L) is Element of bool the carrier of L
bool the carrier of L is non empty set
{(Bottom L)} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {(Bottom L)} is Element of bool the carrier of L
y is set
cx is Element of the carrier of L
L is non empty antisymmetric upper-bounded RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
downarrow (Top L) is Element of bool the carrier of L
bool the carrier of L is non empty set
{(Top L)} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {(Top L)} is Element of bool the carrier of L
y is set
cx is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
B is Element of the carrier of L
wayabove B is upper Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : B is_way_below b1 } is set
x is Element of the carrier of L
wayabove x is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : x is_way_below b1 } is set
(wayabove B) "\/" (wayabove x) is upper Element of bool the carrier of L
B "\/" x is Element of the carrier of L
uparrow (B "\/" x) is non empty filtered upper Element of bool the carrier of L
{(B "\/" x)} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {(B "\/" x)} is non empty upper Element of bool the carrier of L
{B} is non empty trivial finite 1 -element Element of bool the carrier of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
{B} "\/" {x} is non empty Element of bool the carrier of L
uparrow B is non empty filtered upper Element of bool the carrier of L
uparrow {B} is non empty upper Element of bool the carrier of L
uparrow x is non empty filtered upper Element of bool the carrier of L
uparrow {x} is non empty upper Element of bool the carrier of L
(uparrow B) "\/" (uparrow x) is non empty filtered upper Element of bool the carrier of L
uparrow ((uparrow B) "\/" (uparrow x)) is non empty filtered upper Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
B is Element of the carrier of L
waybelow B is lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
x is Element of the carrier of L
waybelow x is lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below x } is set
(waybelow B) "/\" (waybelow x) is lower Element of bool the carrier of L
B "/\" x is Element of the carrier of L
downarrow (B "/\" x) is non empty directed lower Element of bool the carrier of L
{(B "/\" x)} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {(B "/\" x)} is non empty lower Element of bool the carrier of L
{B} is non empty trivial finite 1 -element Element of bool the carrier of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
{B} "/\" {x} is non empty Element of bool the carrier of L
downarrow B is non empty directed lower Element of bool the carrier of L
downarrow {B} is non empty lower Element of bool the carrier of L
downarrow x is non empty directed lower Element of bool the carrier of L
downarrow {x} is non empty lower Element of bool the carrier of L
(downarrow B) "/\" (downarrow x) is non empty directed lower Element of bool the carrier of L
downarrow ((downarrow B) "/\" (downarrow x)) is non empty directed lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
B is Element of the carrier of L
L ~ is non empty strict reflexive transitive antisymmetric RelStr
B ~ is Element of the carrier of (L ~)
the carrier of (L ~) is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x "\/" y is Element of the carrier of L
(x "\/" y) ~ is Element of the carrier of (L ~)
x ~ is Element of the carrier of (L ~)
y ~ is Element of the carrier of (L ~)
(x ~) "/\" (y ~) is Element of the carrier of (L ~)
x is Element of the carrier of (L ~)
y is Element of the carrier of (L ~)
x "/\" y is Element of the carrier of (L ~)
~ (x "/\" y) is Element of the carrier of L
~ x is Element of the carrier of L
~ y is Element of the carrier of L
(~ x) "\/" (~ y) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is non empty Element of bool the carrier of L
"/\" (B,L) is Element of the carrier of L
downarrow ("/\" (B,L)) is non empty directed lower Element of bool the carrier of L
{("/\" (B,L))} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {("/\" (B,L))} is non empty lower Element of bool the carrier of L
{ (downarrow b1) where b1 is Element of the carrier of L : b1 in B } is set
meet { (downarrow b1) where b1 is Element of the carrier of L : b1 in B } is set
y is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
cx is set
dx is Element of the carrier of L
downarrow dx is non empty directed lower Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {dx} is non empty lower Element of bool the carrier of L
cx is Element of the carrier of L
downarrow cx is non empty directed lower Element of bool the carrier of L
{cx} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {cx} is non empty lower Element of bool the carrier of L
dx is Element of bool (bool the carrier of L)
GB is set
X is Element of the carrier of L
G is set
dy is Element of bool (bool the carrier of L)
k is Element of the carrier of L
downarrow k is non empty directed lower Element of bool the carrier of L
{k} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {k} is non empty lower Element of bool the carrier of L
meet dy is Element of bool the carrier of L
G is Element of the carrier of L
downarrow G is non empty directed lower Element of bool the carrier of L
{G} is non empty trivial finite 1 -element Element of bool the carrier of L
downarrow {G} is non empty lower Element of bool the carrier of L
X is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is non empty Element of bool the carrier of L
"\/" (B,L) is Element of the carrier of L
uparrow ("\/" (B,L)) is non empty filtered upper Element of bool the carrier of L
{("\/" (B,L))} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {("\/" (B,L))} is non empty upper Element of bool the carrier of L
{ (uparrow b1) where b1 is Element of the carrier of L : b1 in B } is set
meet { (uparrow b1) where b1 is Element of the carrier of L : b1 in B } is set
y is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
cx is set
dx is Element of the carrier of L
uparrow dx is non empty filtered upper Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {dx} is non empty upper Element of bool the carrier of L
cx is Element of the carrier of L
uparrow cx is non empty filtered upper Element of bool the carrier of L
{cx} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {cx} is non empty upper Element of bool the carrier of L
dx is Element of bool (bool the carrier of L)
GB is set
X is Element of the carrier of L
G is set
dy is Element of bool (bool the carrier of L)
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of bool the carrier of L
{k} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {k} is non empty upper Element of bool the carrier of L
meet dy is Element of bool the carrier of L
G is Element of the carrier of L
uparrow G is non empty filtered upper Element of bool the carrier of L
{G} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {G} is non empty upper Element of bool the carrier of L
X is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
B is Element of the carrier of L
compactbelow B is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : ( b1 <= B & b1 is compact ) } is set
y is Element of the carrier of L
cx is Element of the carrier of L
y "\/" cx is Element of the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
B is non empty irreducible Element of bool the carrier of L
B ` is Element of bool the carrier of L
the carrier of L \ B is set
x is Element of the carrier of (InclPoset the topology of L)
cx is Element of the carrier of (InclPoset the topology of L)
dx is Element of the carrier of (InclPoset the topology of L)
cx "/\" dx is Element of the carrier of (InclPoset the topology of L)
dy is Element of bool the carrier of L
GB is Element of bool the carrier of L
dy /\ GB is Element of bool the carrier of L
cx /\ dx is set
cx "/\" dx is Element of the carrier of (InclPoset the topology of L)
(dy /\ GB) ` is Element of bool the carrier of L
the carrier of L \ (dy /\ GB) is set
dy ` is Element of bool the carrier of L
the carrier of L \ dy is set
GB ` is Element of bool the carrier of L
the carrier of L \ GB is set
(dy `) \/ (GB `) is Element of bool the carrier of L
((dy `) \/ (GB `)) /\ B is Element of bool the carrier of L
(dy `) /\ B is Element of bool the carrier of L
(GB `) /\ B is Element of bool the carrier of L
((dy `) /\ B) \/ ((GB `) /\ B) is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
B is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
B "\/" x is Element of the carrier of (InclPoset the topology of L)
B \/ x is set
B "/\" x is Element of the carrier of (InclPoset the topology of L)
B /\ x is set
y is Element of bool the carrier of L
cx is Element of bool the carrier of L
y \/ cx is Element of bool the carrier of L
y /\ cx is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
B is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
x /\ y is set
x "/\" y is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
x "/\" y is Element of the carrier of (InclPoset the topology of L)
x "/\" y is Element of the carrier of (InclPoset the topology of L)
x /\ y is set
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
B is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
x \/ y is set
x "\/" y is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
x "\/" y is Element of the carrier of (InclPoset the topology of L)
x \/ y is set
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
B is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
x "\/" y is Element of the carrier of (InclPoset the topology of L)
B "/\" (x "\/" y) is Element of the carrier of (InclPoset the topology of L)
B "/\" x is Element of the carrier of (InclPoset the topology of L)
B "/\" y is Element of the carrier of (InclPoset the topology of L)
(B "/\" x) "\/" (B "/\" y) is Element of the carrier of (InclPoset the topology of L)
x "\/" y is Element of the carrier of (InclPoset the topology of L)
B "/\" (x "\/" y) is Element of the carrier of (InclPoset the topology of L)
B /\ (x "\/" y) is set
x \/ y is set
B /\ (x \/ y) is set
B /\ x is set
B /\ y is set
(B /\ x) \/ (B /\ y) is set
B "/\" x is Element of the carrier of (InclPoset the topology of L)
(B "/\" x) \/ (B /\ y) is set
B "/\" y is Element of the carrier of (InclPoset the topology of L)
(B "/\" x) \/ (B "/\" y) is set
(B "/\" x) "\/" (B "/\" y) is Element of the carrier of (InclPoset the topology of L)
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
B is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr
the carrier of B is non empty set
bool the carrier of B is non empty set
bool (bool the carrier of B) is non empty set
the topology of B is non empty Element of bool (bool the carrier of B)
TopStruct(# the carrier of B, the topology of B #) is non empty strict TopSpace-like TopStruct
x is Element of the carrier of L
y is Element of the carrier of B
cx is Element of bool (bool the carrier of B)
Intersect cx is Element of bool the carrier of B
dy is Element of bool the carrier of B
dy is Element of bool the carrier of L
GB is Element of bool the carrier of B
X is Element of bool the carrier of B
G is Element of bool the carrier of L
k is Element of bool the carrier of L
dx is Element of bool (bool the carrier of L)
L is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is Element of the carrier of L
uparrow B is non empty filtered upper Element of bool the carrier of L
{B} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {B} is non empty upper Element of bool the carrier of L
bool (bool the carrier of L) is non empty set
y is Element of bool (bool the carrier of L)
union y is Element of bool the carrier of L
cx is set
dx is Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element Element of bool (bool the carrier of L)
dy is Element of bool (bool the carrier of L)
GB is Element of bool (bool the carrier of L)
union GB is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete RelStr
sigma L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is non empty Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
B is Element of bool the carrier of L
the topology of L is non empty Element of bool (bool the carrier of L)
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
B is filtered Element of bool the carrier of L
{ (downarrow b1) where b1 is Element of the carrier of L : b1 in B } is set
x is Element of bool (bool the carrier of L)
COMPLEMENT x is Element of bool (bool the carrier of L)
y is Element of bool the carrier of (InclPoset (sigma L))
dx is Element of the carrier of (InclPoset (sigma L))
dy is Element of the carrier of (InclPoset (sigma L))
the topology of L is non empty Element of bool (bool the carrier of L)
GB is Element of bool the carrier of L
GB ` is Element of bool the carrier of L
the carrier of L \ GB is set
G is Element of the carrier of L
downarrow G is non empty directed lower property(S) Element of bool the carrier of L
{G} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {G} is non empty lower property(S) Element of bool the carrier of L
X is Element of bool the carrier of L
X ` is Element of bool the carrier of L
the carrier of L \ X is set
k is Element of the carrier of L
downarrow k is non empty directed lower property(S) Element of bool the carrier of L
{k} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {k} is non empty lower property(S) Element of bool the carrier of L
Bx is Element of the carrier of L
downarrow Bx is non empty directed lower property(S) Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {Bx} is non empty lower property(S) Element of bool the carrier of L
(downarrow Bx) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow Bx) is set
Bx is Element of the carrier of (InclPoset (sigma L))
(downarrow k) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow k) is set
(downarrow G) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow G) is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
B is Element of bool the carrier of (InclPoset (sigma L))
x is filtered Element of bool the carrier of L
{ ((downarrow b1) `) where b1 is Element of the carrier of L : b1 in x } is set
{ (downarrow b1) where b1 is Element of the carrier of L : b1 in x } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
cx is set
dx is Element of the carrier of L
downarrow dx is non empty directed lower property(S) Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {dx} is non empty lower property(S) Element of bool the carrier of L
cx is Element of bool (bool the carrier of L)
dy is set
GB is Element of the carrier of L
downarrow GB is non empty directed lower property(S) Element of bool the carrier of L
{GB} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {GB} is non empty lower property(S) Element of bool the carrier of L
(downarrow GB) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow GB) is set
dy is Element of bool (bool the carrier of L)
X is set
GB is Element of bool (bool the carrier of L)
G is Element of the carrier of L
downarrow G is non empty directed lower property(S) Element of bool the carrier of L
{G} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {G} is non empty lower property(S) Element of bool the carrier of L
(downarrow G) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow G) is set
dx is Element of bool (bool the carrier of L)
COMPLEMENT dx is Element of bool (bool the carrier of L)
G is Element of bool the carrier of L
G ` is Element of bool the carrier of L
the carrier of L \ G is set
k is Element of the carrier of L
downarrow k is non empty directed lower property(S) Element of bool the carrier of L
{k} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {k} is non empty lower property(S) Element of bool the carrier of L
(downarrow k) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow k) is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
B is Element of the carrier of L
x is Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
y is non empty directed Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
cx is Element of the carrier of L
dx is Element of the carrier of L
L is non empty reflexive RelStr
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
the carrier of L is non empty set
[: the carrier of [:L,L:], the carrier of L:] is set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
B is Element of bool the carrier of L
x is Element of the carrier of (InclPoset (sigma L))
the topology of L is non empty Element of bool (bool the carrier of L)
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is non empty Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
y is Element of the carrier of L
cx is Element of the carrier of L
downarrow cx is non empty directed lower property(S) Element of bool the carrier of L
{cx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {cx} is non empty lower property(S) Element of bool the carrier of L
(downarrow cx) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow cx) is set
downarrow y is non empty directed lower property(S) Element of bool the carrier of L
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {y} is non empty lower property(S) Element of bool the carrier of L
(downarrow y) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow y) is set
dx is Element of the carrier of (InclPoset (sigma L))
dy is Element of the carrier of (InclPoset (sigma L))
dy "\/" dx is Element of the carrier of (InclPoset (sigma L))
y "/\" cx is Element of the carrier of L
GB is Element of the carrier of L
dy \/ dx is set
(downarrow y) /\ (downarrow cx) is Element of bool the carrier of L
((downarrow y) /\ (downarrow cx)) ` is Element of bool the carrier of L
the carrier of L \ ((downarrow y) /\ (downarrow cx)) is set
downarrow (y "/\" cx) is non empty directed lower property(S) Element of bool the carrier of L
{(y "/\" cx)} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {(y "/\" cx)} is non empty lower property(S) Element of bool the carrier of L
(downarrow (y "/\" cx)) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow (y "/\" cx)) is set
((downarrow (y "/\" cx)) `) ` is lower inaccessible_by_directed_joins property(S) Element of bool the carrier of L
the carrier of L \ ((downarrow (y "/\" cx)) `) is set
B /\ (((downarrow (y "/\" cx)) `) `) is Element of bool the carrier of L
B /\ (downarrow (y "/\" cx)) is Element of bool the carrier of L
X is set
G is Element of the carrier of L
y is Element of the carrier of (InclPoset (sigma L))
cx is Element of the carrier of (InclPoset (sigma L))
y "\/" cx is Element of the carrier of (InclPoset (sigma L))
dy is Element of bool the carrier of L
dx is Element of bool the carrier of L
dx \/ dy is Element of bool the carrier of L
y \/ cx is set
GB is set
X is set
G is Element of the carrier of L
k is Element of the carrier of L
G "/\" k is Element of the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
B is Element of bool the carrier of L
x is Element of the carrier of (InclPoset (sigma L))
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is non empty Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
y is Element of the carrier of L
downarrow y is non empty directed lower property(S) Element of bool the carrier of L
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {y} is non empty lower property(S) Element of bool the carrier of L
(downarrow y) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow y) is set
Cl {y} is closed Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
sup_op L is V22() V25( the carrier of [:L,L:]) V26( the carrier of L) Function-like V36( the carrier of [:L,L:], the carrier of L) Element of bool [: the carrier of [:L,L:], the carrier of L:]
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
[: the carrier of [:L,L:], the carrier of L:] is set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
B is Element of bool the carrier of L
x is Element of the carrier of (InclPoset (sigma L))
the topology of L is non empty Element of bool (bool the carrier of L)
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
B ` is Element of bool the carrier of L
the carrier of L \ B is set
the topology of (ConvergenceSpace (Scott-Convergence L)) is non empty Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
[:L,L:] is non empty strict TopSpace-like TopStruct
dx is Element of the carrier of L
dy is Element of the carrier of L
dx "\/" dy is Element of the carrier of L
the carrier of [:L,L:] is non empty set
[: the carrier of [:L,L:], the carrier of L:] is non empty set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
GB is V22() V25( the carrier of [:L,L:]) V26( the carrier of L) Function-like V36( the carrier of [:L,L:], the carrier of L) Element of bool [: the carrier of [:L,L:], the carrier of L:]
GB . (dx,dy) is set
[dx,dy] is set
{dx,dy} is non empty finite set
{dx} is non empty trivial finite 1 -element set
{{dx,dy},{dx}} is non empty finite V43() set
GB . [dx,dy] is set
[#] L 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 L
GB " B is Element of bool the carrier of [:L,L:]
bool the carrier of [:L,L:] is non empty set
bool (bool the carrier of [:L,L:]) is non empty set
X is Element of bool (bool the carrier of [:L,L:])
union X is Element of bool the carrier of [:L,L:]
[: the carrier of L, the carrier of L:] is non empty set
[dx,dy] is Element of the carrier of [:L,L:]
G is set
k is Element of bool the carrier of L
Bx is Element of bool the carrier of L
[:k,Bx:] is Element of bool the carrier of [:L,L:]
bool the carrier of [:L,L:] is non empty set
UA is set
GB .: G is Element of bool the carrier of L
UA9 is set
GB . UA9 is set
F is Element of the carrier of L
F9 is Element of the carrier of L
[F,F9] is Element of the carrier of [:L,L:]
{F,F9} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F9},{F}} is non empty finite V43() set
G is Element of the carrier of L
G is Element of the carrier of L
GB . (G,G) is set
[G,G] is set
{G,G} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G},{G}} is non empty finite V43() set
GB . [G,G] is set
G "\/" G is Element of the carrier of L
y is Element of bool the carrier of L
Bx is Element of bool the carrier of L
k /\ Bx is Element of bool the carrier of L
UA9 is Element of the carrier of L
[UA9,UA9] is Element of the carrier of [:L,L:]
{UA9,UA9} is non empty finite set
{UA9} is non empty trivial finite 1 -element set
{{UA9,UA9},{UA9}} is non empty finite V43() set
UA9 "\/" UA9 is Element of the carrier of L
GB . (UA9,UA9) is set
[UA9,UA9] is set
GB . [UA9,UA9] is set
GB .: (GB " B) is Element of bool the carrier of L
"\/" ((B `),L) is Element of the carrier of L
cx is Element of the carrier of L
downarrow cx is non empty directed lower property(S) Element of bool the carrier of L
{cx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {cx} is non empty lower property(S) Element of bool the carrier of L
(downarrow cx) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow cx) is set
(B `) ` is Element of bool the carrier of L
the carrier of L \ (B `) is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sup_op L is V22() V25( the carrier of [:L,L:]) V26( the carrier of L) Function-like V36( the carrier of [:L,L:], the carrier of L) Element of bool [: the carrier of [:L,L:], the carrier of L:]
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
the carrier of L is non empty set
[: the carrier of [:L,L:], the carrier of L:] is set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
x is non empty TopSpace-like TopStruct
the carrier of x 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
TopStruct(# the carrier of x, the topology of x #) is non empty strict TopSpace-like TopStruct
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
[:x,x:] is non empty strict TopSpace-like TopStruct
the carrier of [:x,x:] is non empty set
[: the carrier of [:x,x:], the carrier of x:] is non empty set
bool [: the carrier of [:x,x:], the carrier of x:] is non empty set
[: the carrier of x, the carrier of x:] is non empty set
y is V22() V25( the carrier of [:x,x:]) V26( the carrier of x) Function-like V36( the carrier of [:x,x:], the carrier of x) Element of bool [: the carrier of [:x,x:], the carrier of x:]
the topology of L is non empty Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
dx is Element of the carrier of [:x,x:]
y . dx is Element of the carrier of x
GB is Element of the carrier of x
X is Element of the carrier of x
[GB,X] is Element of the carrier of [:x,x:]
{GB,X} is non empty finite set
{GB} is non empty trivial finite 1 -element set
{{GB,X},{GB}} is non empty finite V43() set
G is Element of the carrier of L
waybelow G is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below G } is set
k is Element of the carrier of L
waybelow k is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below k } is set
(waybelow G) "\/" (waybelow k) is non empty directed Element of bool the carrier of L
dy is Element of the carrier of x
UA9 is a_neighborhood of y . dx
Int UA9 is open Element of bool the carrier of x
UA is Element of the carrier of L
{ (wayabove b1) where b1 is Element of the carrier of L : b1 is_way_below UA } is set
F is open UA -quasi_basis Element of bool (bool the carrier of L)
F9 is Element of bool the carrier of x
G is Element of the carrier of L
wayabove G is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : G is_way_below b1 } is set
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of L : ( b1 in waybelow G & b2 in waybelow k ) } is set
cx is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous Scott TopRelStr
"\/" ((waybelow G),L) is Element of the carrier of L
"\/" ((waybelow k),L) is Element of the carrier of L
y . (GB,X) is set
[GB,X] is set
y . [GB,X] is set
G "\/" k is Element of the carrier of L
"\/" (((waybelow G) "\/" (waybelow k)),L) is Element of the carrier of L
G is Element of the carrier of L
Gg is Element of the carrier of L
U1 is Element of the carrier of L
Gg "\/" U1 is Element of the carrier of L
bool the carrier of [:x,x:] is non empty set
wayabove Gg is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : Gg is_way_below b1 } is set
wayabove U1 is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : U1 is_way_below b1 } is set
[:(wayabove Gg),(wayabove U1):] is upper Element of bool the carrier of [:L,L:]
bool the carrier of [:L,L:] is non empty set
k is Element of bool the carrier of x
U19 is Element of bool the carrier of x
U1 is Element of bool the carrier of [:x,x:]
Int U1 is open Element of bool the carrier of [:x,x:]
[G,k] is Element of the carrier of [:L,L:]
{G,k} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,k},{G}} is non empty finite V43() set
V is a_neighborhood of dx
y .: V is Element of bool the carrier of x
(wayabove Gg) "\/" (wayabove U1) is upper Element of bool the carrier of L
uparrow (Gg "\/" U1) is non empty filtered upper Element of bool the carrier of L
{(Gg "\/" U1)} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {(Gg "\/" U1)} is non empty upper Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sup_op L is V22() V25( the carrier of [:L,L:]) V26( the carrier of L) Function-like V36( the carrier of [:L,L:], the carrier of L) Element of bool [: the carrier of [:L,L:], the carrier of L:]
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
the carrier of L is non empty set
[: the carrier of [:L,L:], the carrier of L:] is set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
bool the carrier of L is non empty set
B is non empty irreducible Element of bool the carrier of L
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
Scott-Convergence L is V22() (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is non empty Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
TopStruct(# the carrier of L, the topology of L #) is non empty strict TopSpace-like TopStruct
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
B ` is Element of bool the carrier of L
the carrier of L \ B is set
x is Element of the carrier of (InclPoset (sigma L))
y is Element of the carrier of L
downarrow y is non empty directed lower property(S) Element of bool the carrier of L
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {y} is non empty lower property(S) Element of bool the carrier of L
(downarrow y) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow y) is set
Cl {y} is closed Element of bool the carrier of L
cx is Element of the carrier of L
{cx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
Cl {cx} is closed Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
uparrow (Bottom L) is non empty filtered upper Element of bool the carrier of L
bool the carrier of L is non empty set
{(Bottom L)} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {(Bottom L)} is non empty upper Element of bool the carrier of L
[#] L 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 L
B is Element of bool the carrier of L
B is Element of the carrier of L
x is Element of bool the carrier of L
y is Element of the carrier of L
cx is Element of the carrier of L
uparrow cx is non empty filtered upper Element of bool the carrier of L
{cx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {cx} is non empty upper Element of bool the carrier of L
{ (wayabove b1) where b1 is Element of the carrier of L : b1 is_way_below y } is set
bool (bool the carrier of L) is non empty set
wayabove cx is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : cx is_way_below b1 } is set
Int (uparrow cx) is open Element of bool the carrier of L
sup_op L is V22() V25( the carrier of [:L,L:]) V26( the carrier of L) Function-like V36( the carrier of [:L,L:], the carrier of L) Element of bool [: the carrier of [:L,L:], the carrier of L:]
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
[: the carrier of [:L,L:], the carrier of L:] is set
bool [: the carrier of [:L,L:], the carrier of L:] is non empty set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
B is Element of bool the carrier of L
{ (wayabove b1) where b1 is Element of the carrier of L : b1 in B } is set
union { (wayabove b1) where b1 is Element of the carrier of L : b1 in B } is set
y is set
cx is Element of the carrier of L
dx is Element of the carrier of L
wayabove dx is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : dx is_way_below b1 } is set
cx is set
dx is Element of the carrier of L
wayabove dx is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : dx is_way_below b1 } is set
uparrow dx is non empty filtered upper Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {dx} is non empty upper Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
B is Element of the carrier of L
waybelow B is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
x is Element of the carrier of L
waybelow x is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below x } is set
B is Element of the carrier of L
waybelow B is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
"\/" ((waybelow B),L) is Element of the carrier of L
downarrow ("\/" ((waybelow B),L)) is non empty directed lower property(S) Element of bool the carrier of L
{("\/" ((waybelow B),L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {("\/" ((waybelow B),L))} is non empty lower property(S) Element of bool the carrier of L
(downarrow ("\/" ((waybelow B),L))) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow ("\/" ((waybelow B),L))) is set
{ (wayabove b1) where b1 is Element of the carrier of L : b1 in (downarrow ("\/" ((waybelow B),L))) ` } is set
union { (wayabove b1) where b1 is Element of the carrier of L : b1 in (downarrow ("\/" ((waybelow B),L))) ` } is set
dx is set
dy is Element of the carrier of L
wayabove dy is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : dy is_way_below b1 } is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
B is Element of the carrier of L
{ b1 where b1 is Element of bool the carrier of L : ex b2 being Element of the carrier of L st
( b1 c= wayabove b2 & b2 is_way_below B & B in b1 & b1 is open & b1 is filtered ) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
y is set
cx is Element of bool the carrier of L
dx is Element of the carrier of L
wayabove dx is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : dx is_way_below b1 } is set
y is Element of bool (bool the carrier of L)
{ (wayabove b1) where b1 is Element of the carrier of L : b1 is_way_below B } is set
cx is Element of bool (bool the carrier of L)
dy is Element of bool the carrier of L
GB is Element of bool the carrier of L
X is Element of the carrier of L
wayabove X is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : X is_way_below b1 } is set
Intersect cx is Element of bool the carrier of L
dy is set
GB is Element of bool the carrier of L
X is Element of the carrier of L
wayabove X is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : X is_way_below b1 } is set
meet cx is Element of bool the carrier of L
dy is Element of bool the carrier of L
dx is open B -quasi_basis Element of bool (bool the carrier of L)
GB is Element of bool the carrier of L
X is Element of the carrier of L
wayabove X is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : X is_way_below b1 } is set
G is non empty filtered upper Open Element of bool the carrier of L
dy is Element of bool the carrier of L
GB is Element of bool the carrier of L
X is Element of the carrier of L
wayabove X is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : X is_way_below b1 } is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
x is Element of the carrier of (InclPoset the topology of L)
waybelow x is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below x } is set
"\/" ((waybelow x),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
{ (wayabove b1) where b1 is Element of the carrier of L : b1 in x } is set
union { (wayabove b1) where b1 is Element of the carrier of L : b1 in x } is set
dx is set
dy is set
GB is Element of the carrier of L
wayabove GB is upper Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : GB is_way_below b1 } is set
X is Element of the carrier of (InclPoset the topology of L)
G is non empty directed Element of bool the carrier of (InclPoset the topology of L)
"\/" (G,(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
union G is set
k is set
Bx is Element of bool the carrier of L
uparrow GB is non empty filtered upper Element of bool the carrier of L
{GB} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {GB} is non empty upper Element of bool the carrier of L
Bx is Element of the carrier of (InclPoset the topology of L)
union (waybelow x) is set
dy is set
GB is Element of the carrier of (InclPoset the topology of L)
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
B is Element of the carrier of L
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L) is Element of the carrier of L
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
downarrow ("\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L)) is non empty directed lower property(S) Element of bool the carrier of L
{("\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {("\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L))} is non empty lower property(S) Element of bool the carrier of L
(downarrow ("\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L))) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow ("\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L))) is set
dy is Element of the carrier of L
GB is Element of bool the carrier of L
"/\" (GB,L) is Element of the carrier of L
dy is Element of the carrier of (InclPoset the topology of L)
waybelow dy is non empty directed lower Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : b1 is_way_below dy } is set
"\/" ((waybelow dy),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
union (waybelow dy) is set
GB is set
X is Element of the carrier of (InclPoset the topology of L)
k is open B -quasi_basis Element of bool (bool the carrier of L)
G is Element of bool the carrier of L
Bx is Element of bool the carrier of L
{ (downarrow b1) where b1 is Element of the carrier of L : b1 in Bx } is set
downarrow B is non empty directed lower property(S) Element of bool the carrier of L
{B} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {B} is non empty lower property(S) Element of bool the carrier of L
bool the carrier of L is non empty Element of bool (bool the carrier of L)
y is set
UA is Element of the carrier of L
downarrow UA is non empty directed lower property(S) Element of bool the carrier of L
{UA} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {UA} is non empty lower property(S) Element of bool the carrier of L
y is non empty Element of bool (bool the carrier of L)
COMPLEMENT y is Element of bool (bool the carrier of L)
UA is set
UA9 is Element of bool the carrier of L
UA9 ` is Element of bool the carrier of L
the carrier of L \ UA9 is set
F is Element of the carrier of L
downarrow F is non empty directed lower property(S) Element of bool the carrier of L
{F} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {F} is non empty lower property(S) Element of bool the carrier of L
(downarrow F) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow F) is set
UA is Element of bool the carrier of (InclPoset the topology of L)
"/\" (Bx,L) is Element of the carrier of L
downarrow ("/\" (Bx,L)) is non empty directed lower property(S) Element of bool the carrier of L
{("/\" (Bx,L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {("/\" (Bx,L))} is non empty lower property(S) Element of bool the carrier of L
(downarrow ("/\" (Bx,L))) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow ("/\" (Bx,L))) is set
meet y is Element of bool the carrier of L
union (COMPLEMENT y) is Element of bool the carrier of L
"\/" (UA,(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
(downarrow B) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow B) is set
UA9 is Element of the carrier of (InclPoset the topology of L)
F is Element of bool the carrier of L
F ` is Element of bool the carrier of L
the carrier of L \ F is set
F9 is Element of the carrier of L
downarrow F9 is non empty directed lower property(S) Element of bool the carrier of L
{F9} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {F9} is non empty lower property(S) Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
B is Element of the carrier of L
waybelow B is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
x is Element of the carrier of L
waybelow x is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below x } is set
B is Element of the carrier of L
waybelow B is non empty directed lower property(S) Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below B } is set
"\/" ((waybelow B),L) is Element of the carrier of L
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } is set
y is set
cx is Element of bool the carrier of L
"/\" (cx,L) is Element of the carrier of L
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( B in b1 & b1 in sigma L ) } ,L) is Element of the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
sigma L is non empty Element of bool (bool the carrier of L)
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
x is Element of the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of bool the carrier of L : ( b1 c= x & ex b2 being Element of the carrier of L ex b3 being open b2 -quasi_basis Element of bool (bool the carrier of L) st
( b2 in x & b1 in b3 & ( for b4 being Element of bool the carrier of L holds
( not b4 in b3 or ( b4 is open & b4 is filtered ) ) ) ) ) } is set
cx is set
dx is Element of bool the carrier of L
dy is Element of the carrier of L
GB is open dy -quasi_basis Element of bool (bool the carrier of L)
cx is Element of bool the carrier of (InclPoset (sigma L))
dy is Element of bool the carrier of L
GB is set
X is Element of the carrier of L
G is open X -quasi_basis Element of bool (bool the carrier of L)
k is Element of bool the carrier of L
dx is Element of bool the carrier of (InclPoset (sigma L))
union dx is set
X is set
k is Element of the carrier of L
G is Element of bool the carrier of L
Bx is open k -quasi_basis Element of bool (bool the carrier of L)
"\/" (dx,(InclPoset (sigma L))) is Element of the carrier of (InclPoset (sigma L))
GB is Element of the carrier of (InclPoset (sigma L))
X is Element of bool the carrier of L
G is Element of the carrier of L
k is open G -quasi_basis Element of bool (bool the carrier of L)
x is Element of the carrier of L
{ b1 where b1 is Element of the carrier of (InclPoset (sigma L)) : ( x in b1 & b1 is co-prime ) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
cx is set
dx is Element of the carrier of (InclPoset (sigma L))
cx is Element of bool (bool the carrier of L)
dx is Element of bool (bool the carrier of L)
dy is Element of bool the carrier of L
GB is Element of the carrier of (InclPoset (sigma L))
Intersect dx is Element of bool the carrier of L
dy is set
GB is Element of the carrier of (InclPoset (sigma L))
Intersect dx is Element of bool the carrier of L
meet dx is Element of bool the carrier of L
Intersect dx is Element of bool the carrier of L
Intersect dx is Element of bool the carrier of L
dy is Element of bool the carrier of L
bool the carrier of (InclPoset the topology of L) is non empty set
GB is Element of the carrier of (InclPoset the topology of L)
X is Element of bool the carrier of (InclPoset the topology of L)
"\/" (X,(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
union X is set
G is set
k is Element of bool the carrier of L
Bx is Element of the carrier of (InclPoset the topology of L)
dy is open x -quasi_basis Element of bool (bool the carrier of L)
GB is Element of bool the carrier of L
X is Element of the carrier of (InclPoset (sigma L))
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
B is Element of the carrier of (InclPoset (sigma L))
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
(InclPoset (sigma L)) ~ is non empty strict reflexive transitive antisymmetric RelStr
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
CompactSublatt L is non empty strict reflexive transitive antisymmetric V113(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
{ (uparrow b1) where b1 is Element of the carrier of L : b1 in the carrier of (CompactSublatt L) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
x is set
y is Element of the carrier of L
uparrow y is non empty filtered upper Element of bool the carrier of L
{y} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {y} is non empty upper Element of bool the carrier of L
x is Element of bool (bool the carrier of L)
y is Element of bool (bool the carrier of L)
the topology of L is non empty Element of bool (bool the carrier of L)
cx is set
dx is Element of the carrier of L
uparrow dx is non empty filtered upper Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {dx} is non empty upper Element of bool the carrier of L
cx is Element of the carrier of L
{ (uparrow b1) where b1 is Element of the carrier of L : ( uparrow b1 in y & cx in uparrow b1 ) } is set
dy is set
GB is Element of the carrier of L
uparrow GB is non empty filtered upper Element of bool the carrier of L
{GB} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {GB} is non empty upper Element of bool the carrier of L
dy is Element of bool (bool the carrier of L)
GB is Element of bool (bool the carrier of L)
X is Element of bool the carrier of L
G is Element of the carrier of L
uparrow G is non empty filtered upper Element of bool the carrier of L
{G} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {G} is non empty upper Element of bool the carrier of L
Intersect GB is Element of bool the carrier of L
X is set
G is Element of the carrier of L
uparrow G is non empty filtered upper Element of bool the carrier of L
{G} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {G} is non empty upper Element of bool the carrier of L
Intersect GB is Element of bool the carrier of L
meet GB is Element of bool the carrier of L
Intersect GB is Element of bool the carrier of L
Intersect GB is Element of bool the carrier of L
G is Element of bool the carrier of L
X is Element of the carrier of L
compactbelow X is non empty directed Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 <= X & b1 is compact ) } is set
"\/" ((compactbelow X),L) is Element of the carrier of L
k is set
downarrow X is non empty directed lower property(S) Element of bool the carrier of L
{X} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {X} is non empty lower property(S) Element of bool the carrier of L
(downarrow X) /\ the carrier of (CompactSublatt L) is Element of bool the carrier of L
Bx is Element of the carrier of L
uparrow Bx is non empty filtered upper Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {Bx} is non empty upper Element of bool the carrier of L
Bx is non empty filtered upper Element of bool the carrier of L
X is open cx -quasi_basis Element of bool (bool the carrier of L)
G is open cx -quasi_basis Element of bool (bool the carrier of L)
k is set
Bx is Element of the carrier of L
uparrow Bx is non empty filtered upper Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {Bx} is non empty upper Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
CompactSublatt L is non empty strict reflexive transitive antisymmetric V113(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
{ (uparrow b1) where b1 is Element of the carrier of L : b1 in the carrier of (CompactSublatt L) } is set
sigma L is non empty Element of bool (bool the carrier of L)
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
B is open V99(L) Element of bool (bool the carrier of L)
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
cx is Element of the carrier of (InclPoset (sigma L))
compactbelow cx is Element of bool the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of the carrier of (InclPoset (sigma L)) : ( b1 <= cx & b1 is compact ) } is set
dx is Element of the carrier of (InclPoset (sigma L))
compactbelow dx is Element of bool the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of the carrier of (InclPoset (sigma L)) : ( b1 <= dx & b1 is compact ) } is set
cx is Element of the carrier of (InclPoset (sigma L))
compactbelow cx is Element of bool the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of the carrier of (InclPoset (sigma L)) : ( b1 <= cx & b1 is compact ) } is set
"\/" ((compactbelow cx),(InclPoset (sigma L))) is Element of the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of bool the carrier of L : ( b1 in B & b1 c= cx ) } is set
GB is Element of bool the carrier of L
union { b1 where b1 is Element of bool the carrier of L : ( b1 in B & b1 c= cx ) } is set
X is set
G is set
k is Element of bool the carrier of L
Bx is Element of the carrier of L
uparrow Bx is non empty filtered upper Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {Bx} is non empty upper Element of bool the carrier of L
y is Element of bool the carrier of L
Bx is Element of the carrier of (InclPoset (sigma L))
union (compactbelow cx) is set
G is set
k is Element of the carrier of (InclPoset (sigma L))
cx is Element of the carrier of (InclPoset (sigma L))
{ b1 where b1 is Element of bool the carrier of L : ( b1 in B & b1 c= cx ) } is set
GB is set
X is Element of bool the carrier of L
GB is Element of bool the carrier of (InclPoset (sigma L))
"\/" (GB,(InclPoset (sigma L))) is Element of the carrier of (InclPoset (sigma L))
dx is Element of bool the carrier of L
union GB is set
X is Element of the carrier of (InclPoset (sigma L))
G is Element of bool the carrier of L
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of bool the carrier of L
{k} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {k} is non empty upper Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
sigma L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset (sigma L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (sigma L)) is non empty set
bool the carrier of (InclPoset (sigma L)) is non empty set
CompactSublatt L is non empty strict reflexive transitive antisymmetric V113(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
{ (uparrow b1) where b1 is Element of the carrier of L : b1 in the carrier of (CompactSublatt L) } is set
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete distributive with_suprema with_infima complete RelStr
bool the carrier of L is non empty Element of bool (bool the carrier of L)
cx is set
dx is Element of the carrier of L
uparrow dx is non empty filtered upper Element of bool the carrier of L
{dx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {dx} is non empty upper Element of bool the carrier of L
cx is Element of bool (bool the carrier of L)
dy is Element of bool (bool the carrier of L)
GB is set
X is Element of the carrier of L
uparrow X is non empty filtered upper Element of bool the carrier of L
{X} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {X} is non empty upper Element of bool the carrier of L
dx is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
GB is Element of the carrier of L
GB is Element of the carrier of L
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( GB in b1 & b1 in sigma L ) } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : ( GB in b1 & b1 in sigma L ) } ,L) is Element of the carrier of L
GB is Element of the carrier of L
{ (uparrow b1) where b1 is Element of the carrier of L : ( uparrow b1 in dy & GB in uparrow b1 ) } is set
G is set
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of bool the carrier of L
{k} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {k} is non empty upper Element of bool the carrier of L
G is Element of bool (bool the carrier of L)
k is Element of bool (bool the carrier of L)
Bx is Element of bool the carrier of L
Bx is Element of the carrier of L
uparrow Bx is non empty filtered upper Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {Bx} is non empty upper Element of bool the carrier of L
Intersect k is Element of bool the carrier of L
Bx is set
Bx is Element of the carrier of L
uparrow Bx is non empty filtered upper Element of bool the carrier of L
{Bx} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {Bx} is non empty upper Element of bool the carrier of L
Intersect k is Element of bool the carrier of L
meet k is Element of bool the carrier of L
Intersect k is Element of bool the carrier of L
Intersect k is Element of bool the carrier of L
Bx is Element of bool the carrier of L
the carrier of (InclPoset the topology of L) is non empty non trivial set
Bx is Element of the carrier of (InclPoset the topology of L)
compactbelow Bx is non empty directed Element of bool the carrier of (InclPoset the topology of L)
bool the carrier of (InclPoset the topology of L) is non empty set
{ b1 where b1 is Element of the carrier of (InclPoset the topology of L) : ( b1 <= Bx & b1 is compact ) } is set
"\/" ((compactbelow Bx),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
union (compactbelow Bx) is set
y is set
UA is Element of the carrier of (InclPoset the topology of L)
F is Element of bool the carrier of (InclPoset (sigma L))
"\/" (F,(InclPoset (sigma L))) is Element of the carrier of (InclPoset (sigma L))
union F is set
F9 is Element of bool (bool the carrier of L)
G is Element of bool the carrier of L
bool F9 is non empty set
G is finite Element of bool F9
union G is set
G is finite Element of bool (bool the carrier of L)
union G is Element of bool the carrier of L
Gg is finite Element of bool (bool the carrier of L)
union Gg is Element of bool the carrier of L
U1 is set
U1 is Element of the carrier of (InclPoset (sigma L))
U19 is Element of bool the carrier of L
"/\" (U19,L) is Element of the carrier of L
uparrow ("/\" (U19,L)) is non empty filtered upper Element of bool the carrier of L
{("/\" (U19,L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {("/\" (U19,L))} is non empty upper Element of bool the carrier of L
V is set
u is Element of the carrier of L
{ ((downarrow b1) `) where b1 is Element of the carrier of L : b1 in U19 } is set
u is set
u is Element of the carrier of L
downarrow u is non empty directed lower property(S) Element of bool the carrier of L
{u} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {u} is non empty lower property(S) Element of bool the carrier of L
(downarrow u) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow u) is set
u is set
u is Element of the carrier of L
downarrow u is non empty directed lower property(S) Element of bool the carrier of L
{u} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {u} is non empty lower property(S) Element of bool the carrier of L
(downarrow u) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow u) is set
D is non empty Element of bool the carrier of (InclPoset the topology of L)
union D is set
UA9 is Element of bool the carrier of L
d is set
u is Element of the carrier of L
Uk is set
Uk is Element of the carrier of (InclPoset (sigma L))
Uk9 is Element of bool the carrier of L
u is Element of the carrier of L
downarrow u is non empty directed lower property(S) Element of bool the carrier of L
{u} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {u} is non empty lower property(S) Element of bool the carrier of L
(downarrow u) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow u) is set
u is set
d is Element of the carrier of L
{U19} is non empty trivial finite 1 -element Element of bool (bool the carrier of L)
Gg \ {U19} is finite Element of bool (bool the carrier of L)
union (Gg \ {U19}) is Element of bool the carrier of L
u is set
"\/" (D,(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)
d is Element of the carrier of (InclPoset the topology of L)
u is Element of the carrier of L
downarrow u is non empty directed lower property(S) Element of bool the carrier of L
{u} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {u} is non empty lower property(S) Element of bool the carrier of L
(downarrow u) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow u) is set
V is non empty filtered upper Element of bool the carrier of L
Bx is open GB -quasi_basis Element of bool (bool the carrier of L)
Bx is open GB -quasi_basis Element of bool (bool the carrier of L)
y is set
UA is Element of the carrier of L
uparrow UA is non empty filtered upper Element of bool the carrier of L
{UA} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {UA} is non empty upper Element of bool the carrier of L
GB is open V99(L) Element of bool (bool the carrier of L)
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
CompactSublatt L is non empty strict reflexive transitive antisymmetric V113(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
{ (uparrow b1) where b1 is Element of the carrier of L : b1 in the carrier of (CompactSublatt L) } is set
B is open V99(L) Element of bool (bool the carrier of L)
x is Element of the carrier of L
compactbelow x is non empty directed Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 <= x & b1 is compact ) } is set
y is Element of the carrier of L
compactbelow y is non empty directed Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 <= y & b1 is compact ) } is set
x is Element of the carrier of L
compactbelow x is non empty directed Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 <= x & b1 is compact ) } is set
"\/" ((compactbelow x),L) is Element of the carrier of L
downarrow x is non empty directed lower property(S) Element of bool the carrier of L
{x} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {x} is non empty lower property(S) Element of bool the carrier of L
downarrow ("\/" ((compactbelow x),L)) is non empty directed lower property(S) Element of bool the carrier of L
{("\/" ((compactbelow x),L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {("\/" ((compactbelow x),L))} is non empty lower property(S) Element of bool the carrier of L
GB is Element of the carrier of L
"\/" ((downarrow x),L) is Element of the carrier of L
(downarrow ("\/" ((compactbelow x),L))) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow ("\/" ((compactbelow x),L))) is set
{ b1 where b1 is Element of bool the carrier of L : ( b1 in B & b1 c= (downarrow ("\/" ((compactbelow x),L))) ` ) } is set
(downarrow x) /\ the carrier of (CompactSublatt L) is Element of bool the carrier of L
union { b1 where b1 is Element of bool the carrier of L : ( b1 in B & b1 c= (downarrow ("\/" ((compactbelow x),L))) ` ) } is set
X is set
G is Element of bool the carrier of L
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of bool the carrier of L
{k} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {k} is non empty upper Element of bool the carrier of L