:: WAYBEL14 semantic presentation

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

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

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

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

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

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
"\/" ((),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
"/\" ((),L) is Element of the carrier of L

Bottom L is Element of the carrier of L
the carrier of L is non empty set
uparrow () is Element of bool the carrier of L
bool the carrier of L is non empty set
{()} is non empty trivial finite 1 -element Element of bool the carrier of L
uparrow {()} is Element of bool the carrier of L
y is set
cx is Element of the carrier of L

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

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
() "\/" () 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
() "\/" () is non empty filtered upper Element of bool the carrier of L
uparrow (() "\/" ()) is non empty filtered upper Element of bool the carrier of L

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
() "/\" () 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
() "/\" () is non empty directed lower Element of bool the carrier of L
downarrow (() "/\" ()) is non empty directed lower Element of bool the carrier of L

the carrier of L is non empty set
B is Element of the carrier of L

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

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
{ () where b1 is Element of the carrier of L : b1 in B } is set
meet { () 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

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

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

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

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

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

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

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

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)

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

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

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

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

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)

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)

the carrier of (InclPoset ()) is non empty set
bool the carrier of (InclPoset ()) is non empty set
B is filtered Element of bool the carrier of L
{ () 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 ())
dx is Element of the carrier of (InclPoset ())
dy is Element of the carrier of (InclPoset ())
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
() ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ () is set
Bx is Element of the carrier of (InclPoset ())

the carrier of L \ () is set

the carrier of L \ () is set

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 carrier of (InclPoset ()) is non empty set
bool the carrier of (InclPoset ()) is non empty set
B is Element of bool the carrier of (InclPoset ())
x is filtered Element of bool the carrier of L
{ (() `) where b1 is Element of the carrier of L : b1 in x } is set
{ () 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
() ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ () 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

the carrier of L \ () 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

the carrier of L \ () is set

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

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

the carrier of (InclPoset ()) is non empty set
B is Element of bool the carrier of L
x is Element of the carrier of (InclPoset ())
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

the topology of is non empty Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) 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
() ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ () 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

the carrier of L \ () is set
dx is Element of the carrier of (InclPoset ())
dy is Element of the carrier of (InclPoset ())
dy "\/" dx is Element of the carrier of (InclPoset ())
y "/\" cx is Element of the carrier of L
GB is Element of the carrier of L
dy \/ dx is set
() /\ () is Element of bool the carrier of L
(() /\ ()) ` is Element of bool the carrier of L
the carrier of L \ (() /\ ()) 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 ())
cx is Element of the carrier of (InclPoset ())
y "\/" cx is Element of the carrier of (InclPoset ())
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

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

the carrier of (InclPoset ()) is non empty set
B is Element of bool the carrier of L
x is Element of the carrier of (InclPoset ())

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

the carrier of L \ () is set
Cl {y} is closed Element of bool the carrier of L

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

the carrier of (InclPoset ()) 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 ())
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

B ` is Element of bool the carrier of L
the carrier of L \ B is set
the topology of is non empty Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) 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

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
() ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ () is set
(B `) ` is Element of bool the carrier of L
the carrier of L \ (B `) is 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 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

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

"\/" ((),L) is Element of the carrier of L
"\/" ((),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
"\/" ((() "\/" ()),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

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

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

the carrier of (InclPoset ()) 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 ())
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

the carrier of L \ () 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

Bottom L is Element of the carrier of L
the carrier of L is non empty set
uparrow () is non empty filtered upper Element of bool the carrier of L
bool the carrier of L is non empty set
{()} is non empty trivial finite 1 -element compact Element of bool the carrier of L
uparrow {()} is non empty upper 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

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

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
"\/" ((),L) is Element of the carrier of L
downarrow ("\/" ((),L)) is non empty directed lower property(S) Element of bool the carrier of L
{("\/" ((),L))} is non empty trivial finite 1 -element compact Element of bool the carrier of L
downarrow {("\/" ((),L))} is non empty lower property(S) Element of bool the carrier of L
(downarrow ("\/" ((),L))) ` is upper closed_under_directed_sups Element of bool the carrier of L
the carrier of L \ (downarrow ("\/" ((),L))) is set
{ (wayabove b1) where b1 is Element of the carrier of L : b1 in (downarrow ("\/" ((),L))) ` } is set
union { (wayabove b1) where b1 is Element of the carrier of L : b1 in (downarrow ("\/" ((),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

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

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)

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
"\/" ((),(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 () is set
dy is set
GB is Element of the carrier of (InclPoset the topology 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
sigma L is non empty Element of bool (bool the carrier of L)

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)

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

the carrier of L \ () 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 () 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)

the carrier of L \ () 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

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

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)

the carrier of (InclPoset ()) is non empty set
bool the carrier of (InclPoset ()) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)

the carrier of (InclPoset the topology of L) is non empty non trivial set
x is Element of the carrier of (InclPoset ())
{ 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 ())
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 ())
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 ())) is Element of the carrier of (InclPoset ())
GB is Element of the carrier of (InclPoset ())
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 ()) : ( 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 ())
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 ())
Intersect dx is Element of bool the carrier of L
dy is set
GB is Element of the carrier of (InclPoset ())
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 is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set