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

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

{ b

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

{ b

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

{ b

"\/" ((waybelow B),L) is Element of the carrier of L

wayabove B is Element of bool the carrier of L

{ b

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

{ b

x is Element of the carrier of L

wayabove x is upper Element of bool the carrier of L

{ b

(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

{ b

x is Element of the carrier of L

waybelow x is lower Element of bool the carrier of L

{ b

(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 b

meet { (downarrow b

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 b

meet { (uparrow b

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

{ b

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 b

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 b

{ (downarrow b

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

{ b

k is Element of the carrier of L

waybelow k is non empty directed lower property(S) Element of bool the carrier of L

{ b

(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 b

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

{ b

{ (b

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

{ b

wayabove U1 is upper Element of bool the carrier of L

{ b

[:(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 b

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

wayabove cx is upper Element of bool the carrier of L

{ b

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 b

union { (wayabove b

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

{ b

cx is set

dx is Element of the carrier of L

wayabove dx is upper Element of bool the carrier of L

{ b

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

{ b

x is Element of the carrier of L

waybelow x is non empty directed lower property(S) Element of bool the carrier of L

{ b

B is Element of the carrier of L

waybelow B is non empty directed lower property(S) Element of bool the carrier of L

{ b

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

union { (wayabove b

dx is set

dy is Element of the carrier of L

wayabove dy is upper Element of bool the carrier of L

{ b

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

{ b

( b

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

{ b

y is Element of bool (bool the carrier of L)

{ (wayabove b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

"\/" ((waybelow x),(InclPoset the topology of L)) is Element of the carrier of (InclPoset the topology of L)

{ (wayabove b

union { (wayabove b

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

{ b

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

{ ("/\" (b

"\/" ( { ("/\" (b

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 ("\/" ( { ("/\" (b

{("\/" ( { ("/\" (b

downarrow {("\/" ( { ("/\" (b

(downarrow ("\/" ( { ("/\" (b

the carrier of L \ (downarrow ("\/" ( { ("/\" (b

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

{ b

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

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

{ b

x is Element of the carrier of L

waybelow x is non empty directed lower property(S) Element of bool the carrier of L

{ b

B is Element of the carrier of L

waybelow B is non empty directed lower property(S) Element of bool the carrier of L

{ b

"\/" ((waybelow B),L) is Element of the carrier of L

{ ("/\" (b

y is set

cx is Element of bool the carrier of L

"/\" (cx,L) is Element of the carrier of L

"\/" ( { ("/\" (b

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

{ b

( b

( not b

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

{ b

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