:: YELLOW19 semantic presentation

K37() is set

K10(K37()) is non empty set

{} is set

the empty Relation-like non-empty empty-yielding finite finite-yielding V45() set is empty Relation-like non-empty empty-yielding finite finite-yielding V45() set

1 is non empty set

T is non empty set

BoolePoset T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset T) is non empty non trivial set

K10( the carrier of (BoolePoset T)) is non empty set

Bottom (BoolePoset T) is Element of the carrier of (BoolePoset T)

x is set

F is non empty proper filtered upper Element of K10( the carrier of (BoolePoset T))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is Element of the carrier of T

{ b

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

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

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

x is set

j is a_neighborhood of F

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is Element of the carrier of T

(T,F) is Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

x is set

x is a_neighborhood of F

x is a_neighborhood of F

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is Element of the carrier of T

(T,F) is Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

the a_neighborhood of F is a_neighborhood of F

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

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

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset the carrier of T) is non empty non trivial set

UF is Element of the carrier of (BoolePoset ([#] T))

x is Element of the carrier of (BoolePoset ([#] T))

B is a_neighborhood of F

A is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

Int A is open Element of K10( the carrier of T)

UF is Element of the carrier of (BoolePoset ([#] T))

x is Element of the carrier of (BoolePoset ([#] T))

A is a_neighborhood of F

B is a_neighborhood of F

A /\ B is Element of K10( the carrier of T)

C is Element of the carrier of (BoolePoset ([#] T))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of the carrier of T

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is set

x is a_neighborhood of F

Int x is open Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is Element of the carrier of T

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of K10( the carrier of T)

x is Element of the carrier of T

x is non empty filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

Int F is open Element of K10( the carrier of T)

F \ (Int F) is Element of K10( the carrier of T)

the Element of F \ (Int F) is Element of F \ (Int F)

x is Element of the carrier of T

(T,x) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty NetStr over T

the carrier of F is non empty set

the Element of the carrier of F is Element of the carrier of F

F | the Element of the carrier of F is strict NetStr over T

the mapping of (F | the Element of the carrier of F) is Relation-like the carrier of (F | the Element of the carrier of F) -defined the carrier of T -valued Function-like V38( the carrier of (F | the Element of the carrier of F), the carrier of T) Element of K10(K11( the carrier of (F | the Element of the carrier of F), the carrier of T))

the carrier of (F | the Element of the carrier of F) is set

K11( the carrier of (F | the Element of the carrier of F), the carrier of T) is Relation-like set

K10(K11( the carrier of (F | the Element of the carrier of F), the carrier of T)) is non empty set

rng the mapping of (F | the Element of the carrier of F) is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

T is non empty 1-sorted

F is non empty NetStr over T

the carrier of F is non empty set

the carrier of T is non empty set

x is Element of the carrier of F

F | x is strict NetStr over T

the mapping of (F | x) is Relation-like the carrier of (F | x) -defined the carrier of T -valued Function-like V38( the carrier of (F | x), the carrier of T) Element of K10(K11( the carrier of (F | x), the carrier of T))

the carrier of (F | x) is set

K11( the carrier of (F | x), the carrier of T) is Relation-like set

K10(K11( the carrier of (F | x), the carrier of T)) is non empty set

rng the mapping of (F | x) is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

T is non empty 1-sorted

F is non empty reflexive NetStr over T

x is (T,F)

the carrier of F is non empty set

the carrier of T is non empty set

x is Element of the carrier of F

F | x is non empty reflexive strict NetStr over T

the mapping of (F | x) is non empty Relation-like the carrier of (F | x) -defined the carrier of T -valued Function-like V38( the carrier of (F | x), the carrier of T) Element of K10(K11( the carrier of (F | x), the carrier of T))

the carrier of (F | x) is non empty set

K11( the carrier of (F | x), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | x), the carrier of T)) is non empty set

rng the mapping of (F | x) is non empty Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

T is non empty 1-sorted

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

the carrier of F is non empty set

x is Element of the carrier of F

F | x is non empty transitive strict directed subnet of F

the mapping of (F | x) is non empty Relation-like the carrier of (F | x) -defined the carrier of T -valued Function-like V38( the carrier of (F | x), the carrier of T) Element of K10(K11( the carrier of (F | x), the carrier of T))

the carrier of (F | x) is non empty set

K11( the carrier of (F | x), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | x), the carrier of T)) is non empty set

rng the mapping of (F | x) is non empty Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

x is set

dom the mapping of (F | x) is non empty Element of K10( the carrier of (F | x))

K10( the carrier of (F | x)) is non empty set

x is set

the mapping of (F | x) . x is set

j is Element of the carrier of (F | x)

UF is Element of the carrier of F

x is Element of the carrier of F

(F | x) . j is Element of the carrier of T

the mapping of (F | x) . j is Element of the carrier of T

F . x is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . x is Element of the carrier of T

x is Element of the carrier of F

F . x is Element of the carrier of T

the mapping of F . x is Element of the carrier of T

j is Element of the carrier of (F | x)

(F | x) . j is Element of the carrier of T

the mapping of (F | x) . j is Element of the carrier of T

the mapping of (F | x) . x is set

T is non empty 1-sorted

F is non empty transitive directed NetStr over T

x is (T,F)

the carrier of F is non empty set

the carrier of T is non empty set

x is Element of the carrier of F

F | x is non empty transitive strict directed subnet of F

the mapping of (F | x) is non empty Relation-like the carrier of (F | x) -defined the carrier of T -valued Function-like V38( the carrier of (F | x), the carrier of T) Element of K10(K11( the carrier of (F | x), the carrier of T))

the carrier of (F | x) is non empty set

K11( the carrier of (F | x), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | x), the carrier of T)) is non empty set

rng the mapping of (F | x) is non empty Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

x is Element of the carrier of F

F . x is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . x is Element of the carrier of T

j is Element of the carrier of (F | x)

(F | x) . j is Element of the carrier of T

the mapping of (F | x) . j is Element of the carrier of T

T is non empty 1-sorted

F is non empty transitive directed NetStr over T

the carrier of F is non empty set

the carrier of T is non empty set

x is non empty finite set

meet x is set

x is set

x is (T,F)

j is Element of the carrier of F

F | j is non empty transitive strict directed subnet of F

the mapping of (F | j) is non empty Relation-like the carrier of (F | j) -defined the carrier of T -valued Function-like V38( the carrier of (F | j), the carrier of T) Element of K10(K11( the carrier of (F | j), the carrier of T))

the carrier of (F | j) is non empty set

K11( the carrier of (F | j), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | j), the carrier of T)) is non empty set

rng the mapping of (F | j) is non empty Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

UF is set

x is set

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

K10( the carrier of F) is non empty set

[#] F is non empty non proper lower upper Element of K10( the carrier of F)

x is finite Element of K10( the carrier of F)

j is Element of the carrier of F

F | j is non empty transitive strict directed subnet of F

the mapping of (F | j) is non empty Relation-like the carrier of (F | j) -defined the carrier of T -valued Function-like V38( the carrier of (F | j), the carrier of T) Element of K10(K11( the carrier of (F | j), the carrier of T))

the carrier of (F | j) is non empty set

K11( the carrier of (F | j), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | j), the carrier of T)) is non empty set

rng the mapping of (F | j) is non empty Element of K10( the carrier of T)

UF is (T,F)

x is set

{ b

dom the mapping of (F | j) is non empty Element of K10( the carrier of (F | j))

K10( the carrier of (F | j)) is non empty set

A is set

the mapping of (F | j) . A is set

B is Element of the carrier of (F | j)

C is Element of the carrier of F

c is set

x . c is set

a is Element of the carrier of F

F | a is non empty transitive strict directed subnet of F

the mapping of (F | a) is non empty Relation-like the carrier of (F | a) -defined the carrier of T -valued Function-like V38( the carrier of (F | a), the carrier of T) Element of K10(K11( the carrier of (F | a), the carrier of T))

the carrier of (F | a) is non empty set

K11( the carrier of (F | a), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | a), the carrier of T)) is non empty set

rng the mapping of (F | a) is non empty Element of K10( the carrier of T)

{ b

(F | j) . B is Element of the carrier of T

the mapping of (F | j) . B is Element of the carrier of T

F . C is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . C is Element of the carrier of T

a is Element of the carrier of (F | a)

(F | a) . a is Element of the carrier of T

the mapping of (F | a) . a is Element of the carrier of T

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty NetStr over T

{ b

[#] T is non empty non proper Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

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

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

x is set

j is Element of K10( the carrier of T)

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

InclPoset (bool the carrier of T) is non empty strict reflexive transitive antisymmetric RelStr

RelIncl (bool the carrier of T) is Relation-like bool the carrier of T -defined bool the carrier of T -valued reflexive antisymmetric transitive V33( bool the carrier of T) Element of K10(K11((bool the carrier of T),(bool the carrier of T)))

K11((bool the carrier of T),(bool the carrier of T)) is non empty Relation-like set

K10(K11((bool the carrier of T),(bool the carrier of T))) is non empty set

RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) is strict RelStr

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty NetStr over T

(T,F) is Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

x is set

x is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

T is non empty 1-sorted

F is non empty NetStr over T

(T,F) is Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

the carrier of F is non empty set

the Element of the carrier of F is Element of the carrier of F

UF is Element of the carrier of F

F . UF is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . UF is Element of the carrier of T

j is Element of the carrier of (BoolePoset ([#] T))

UF is Element of the carrier of (BoolePoset ([#] T))

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

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

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

InclPoset (bool the carrier of T) is non empty strict reflexive transitive antisymmetric RelStr

RelIncl (bool the carrier of T) is Relation-like bool the carrier of T -defined bool the carrier of T -valued reflexive antisymmetric transitive V33( bool the carrier of T) Element of K10(K11((bool the carrier of T),(bool the carrier of T)))

K11((bool the carrier of T),(bool the carrier of T)) is non empty Relation-like set

K10(K11((bool the carrier of T),(bool the carrier of T))) is non empty set

RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) is strict RelStr

T is non empty 1-sorted

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

F is non empty transitive directed NetStr over T

(T,F) is non empty upper Element of K10( the carrier of (BoolePoset ([#] T)))

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

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

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

InclPoset (bool the carrier of T) is non empty strict reflexive transitive antisymmetric RelStr

RelIncl (bool the carrier of T) is Relation-like bool the carrier of T -defined bool the carrier of T -valued reflexive antisymmetric transitive V33( bool the carrier of T) Element of K10(K11((bool the carrier of T),(bool the carrier of T)))

K11((bool the carrier of T),(bool the carrier of T)) is non empty Relation-like set

K10(K11((bool the carrier of T),(bool the carrier of T))) is non empty set

RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) is strict RelStr

the carrier of F is non empty set

j is Element of the carrier of F

UF is Element of the carrier of F

j is Element of the carrier of (BoolePoset ([#] T))

UF is Element of the carrier of (BoolePoset ([#] T))

x is Element of the carrier of F

A is Element of the carrier of F

j "/\" UF is Element of the carrier of (BoolePoset ([#] T))

B is Element of the carrier of (BoolePoset ([#] T))

j /\ UF is set

C is Element of the carrier of F

c is Element of the carrier of F

F . c is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . c is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

x is Element of the carrier of T

x is Element of K10( the carrier of T)

j is set

the carrier of F is non empty set

UF is Element of the carrier of F

x is Element of the carrier of F

F . x is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . x is Element of the carrier of T

x is Element of the carrier of T

x is a_neighborhood of x

the carrier of F is non empty set

j is Element of the carrier of F

F | j is non empty transitive strict directed subnet of F

the mapping of (F | j) is non empty Relation-like the carrier of (F | j) -defined the carrier of T -valued Function-like V38( the carrier of (F | j), the carrier of T) Element of K10(K11( the carrier of (F | j), the carrier of T))

the carrier of (F | j) is non empty set

K11( the carrier of (F | j), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | j), the carrier of T)) is non empty set

rng the mapping of (F | j) is non empty Element of K10( the carrier of T)

UF is (T,F)

Int x is open Element of K10( the carrier of T)

x is set

A is Element of the carrier of F

F . A is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . A is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

Lim F is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

{ b

x is Element of the carrier of T

x is Element of K10( the carrier of T)

x is a_neighborhood of x

Int x is open Element of K10( the carrier of T)

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty Element of K10( the carrier of T)

BoolePoset F is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset F) is non empty non trivial set

K10( the carrier of (BoolePoset F)) is non empty set

x is non empty filtered upper Element of K10( the carrier of (BoolePoset F))

{ [b

Top (BoolePoset F) is Element of the carrier of (BoolePoset F)

x is Element of x

j is Element of K10( the carrier of T)

UF is Element of the carrier of T

x is Element of the carrier of T

[x,j] is V35() set

{x,j} is finite set

{x} is finite set

{{x,j},{x}} is finite V45() set

A is non empty set

K11(A,A) is non empty Relation-like set

K10(K11(A,A)) is non empty set

B is Relation-like A -defined A -valued Element of K10(K11(A,A))

C is set

C `1 is set

c is Element of the carrier of T

a is Element of x

[c,a] is V35() set

{c,a} is finite set

{c} is finite set

{{c,a},{c}} is finite V45() set

[c,a] `1 is set

K11(A, the carrier of T) is non empty Relation-like set

K10(K11(A, the carrier of T)) is non empty set

C is Relation-like A -defined the carrier of T -valued Function-like V38(A, the carrier of T) Element of K10(K11(A, the carrier of T))

NetStr(# A,B,C #) is non empty strict NetStr over T

c is non empty strict NetStr over T

the carrier of c is non empty set

a is Element of the carrier of c

a is Element of the carrier of c

a `2 is set

a `2 is set

V is Element of A

b is Element of A

[V,b] is V35() set

{V,b} is finite set

{V} is finite set

{{V,b},{V}} is finite V45() set

the InternalRel of c is Relation-like the carrier of c -defined the carrier of c -valued Element of K10(K11( the carrier of c, the carrier of c))

K11( the carrier of c, the carrier of c) is non empty Relation-like set

K10(K11( the carrier of c, the carrier of c)) is non empty set

b `2 is set

V `2 is set

a is Element of the carrier of c

a is Element of the carrier of c

a `2 is set

a `2 is set

b is Element of the carrier of c

b `2 is set

V is Element of the carrier of c

V `2 is set

a9 is Element of the carrier of c

c . a9 is Element of the carrier of T

the mapping of c is non empty Relation-like the carrier of c -defined the carrier of T -valued Function-like V38( the carrier of c, the carrier of T) Element of K10(K11( the carrier of c, the carrier of T))

K11( the carrier of c, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of c, the carrier of T)) is non empty set

the mapping of c . a9 is Element of the carrier of T

a9 `1 is set

x is non empty strict NetStr over T

the carrier of x is non empty set

j is non empty strict NetStr over T

the carrier of j is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))

K11( the carrier of x, the carrier of x) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of x)) is non empty set

the InternalRel of j is Relation-like the carrier of j -defined the carrier of j -valued Element of K10(K11( the carrier of j, the carrier of j))

K11( the carrier of j, the carrier of j) is non empty Relation-like set

K10(K11( the carrier of j, the carrier of j)) is non empty set

UF is set

x is set

[UF,x] is V35() set

{UF,x} is finite set

{UF} is finite set

{{UF,x},{UF}} is finite V45() set

A is Element of the carrier of x

B is Element of the carrier of x

c is Element of the carrier of j

c `2 is set

C is Element of the carrier of j

C `2 is set

A is Element of the carrier of j

B is Element of the carrier of j

c is Element of the carrier of x

c `2 is set

C is Element of the carrier of x

C `2 is set

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V38( the carrier of x, the carrier of T) Element of K10(K11( the carrier of x, the carrier of T))

K11( the carrier of x, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of T)) is non empty set

the mapping of j is non empty Relation-like the carrier of j -defined the carrier of T -valued Function-like V38( the carrier of j, the carrier of T) Element of K10(K11( the carrier of j, the carrier of T))

K11( the carrier of j, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of j, the carrier of T)) is non empty set

K11( { [b

K10(K11( { [b

x is Relation-like { [b

UF is Relation-like { [b

A is set

x . A is set

UF . A is set

c is Element of { [b

x . c is set

B is Element of the carrier of x

x . B is Element of the carrier of T

the mapping of x . B is Element of the carrier of T

B `1 is set

C is Element of the carrier of j

j . C is Element of the carrier of T

the mapping of j . C is Element of the carrier of T

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty Element of K10( the carrier of T)

BoolePoset F is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset F) is non empty non trivial set

K10( the carrier of (BoolePoset F)) is non empty set

x is non empty filtered upper Element of K10( the carrier of (BoolePoset F))

(T,F,x) is non empty strict NetStr over T

the carrier of (T,F,x) is non empty set

the InternalRel of (T,F,x) is Relation-like the carrier of (T,F,x) -defined the carrier of (T,F,x) -valued Element of K10(K11( the carrier of (T,F,x), the carrier of (T,F,x)))

K11( the carrier of (T,F,x), the carrier of (T,F,x)) is non empty Relation-like set

K10(K11( the carrier of (T,F,x), the carrier of (T,F,x))) is non empty set

x is set

x is set

j is set

[x,x] is V35() set

{x,x} is finite set

{x} is finite set

{{x,x},{x}} is finite V45() set

[x,j] is V35() set

{x,j} is finite set

{x} is finite set

{{x,j},{x}} is finite V45() set

[x,j] is V35() set

{x,j} is finite set

{{x,j},{x}} is finite V45() set

x is Element of the carrier of (T,F,x)

UF is Element of the carrier of (T,F,x)

UF `2 is set

x `2 is set

A is Element of the carrier of (T,F,x)

A `2 is set

x is set

[x,x] is V35() set

{x,x} is finite set

{x} is finite set

{{x,x},{x}} is finite V45() set

x is Element of the carrier of (T,F,x)

x `2 is set

T is non empty 1-sorted

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is non empty Element of K10( the carrier of T)

BoolePoset F is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset F) is non empty non trivial set

K10( the carrier of (BoolePoset F)) is non empty set

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset F))

(T,F,x) is non empty reflexive transitive strict NetStr over T

{ [b

the carrier of (T,F,x) is non empty set

[#] (T,F,x) is non empty non proper lower upper Element of K10( the carrier of (T,F,x))

K10( the carrier of (T,F,x)) is non empty set

x is Element of the carrier of (T,F,x)

j is Element of the carrier of (T,F,x)

UF is Element of the carrier of T

x is Element of x

[UF,x] is V35() set

{UF,x} is finite set

{UF} is finite set

{{UF,x},{UF}} is finite V45() set

B is Element of the carrier of T

C is Element of x

[B,C] is V35() set

{B,C} is finite set

{B} is finite set

{{B,C},{B}} is finite V45() set

A is Element of the carrier of (BoolePoset F)

c is Element of the carrier of (BoolePoset F)

A "/\" c is Element of the carrier of (BoolePoset F)

a is Element of x

the Element of a is Element of a

Bottom (BoolePoset F) is Element of the carrier of (BoolePoset F)

V is Element of the carrier of T

[V,a] is V35() set

{V,a} is finite set

{V} is finite set

{{V,a},{V}} is finite V45() set

b is Element of the carrier of (T,F,x)

[B,c] is V35() set

{B,c} is finite set

{{B,c},{B}} is finite V45() set

[B,c] `2 is set

[V,a] `2 is set

A /\ c is set

[UF,A] is V35() set

{UF,A} is finite set

{{UF,A},{UF}} is finite V45() set

[UF,A] `2 is set

{{}} is finite set

T is non empty 1-sorted

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

F \ {{}} is Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),F) is non empty reflexive transitive strict NetStr over T

(T,(T,([#] T),F)) is non empty upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

the carrier of (T,([#] T),F) is non empty set

{ [b

bool ([#] T) is non empty Element of K10(K10(([#] T)))

K10(([#] T)) is non empty set

K10(K10(([#] T))) is non empty set

InclPoset (bool ([#] T)) is non empty strict reflexive transitive antisymmetric RelStr

x is set

x is Element of K10( the carrier of T)

the Element of x is Element of x

UF is Element of the carrier of T

[UF,x] is V35() set

{UF,x} is finite set

{UF} is finite set

{{UF,x},{UF}} is finite V45() set

x is Element of the carrier of (T,([#] T),F)

A is Element of the carrier of (T,([#] T),F)

(T,([#] T),F) . A is Element of the carrier of T

the mapping of (T,([#] T),F) is non empty Relation-like the carrier of (T,([#] T),F) -defined the carrier of T -valued Function-like V38( the carrier of (T,([#] T),F), the carrier of T) Element of K10(K11( the carrier of (T,([#] T),F), the carrier of T))

K11( the carrier of (T,([#] T),F), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (T,([#] T),F), the carrier of T)) is non empty set

the mapping of (T,([#] T),F) . A is Element of the carrier of T

x `2 is set

A `1 is set

A `2 is set

B is Element of the carrier of T

C is Element of F

[B,C] is V35() set

{B,C} is finite set

{B} is finite set

{{B,C},{B}} is finite V45() set

x is set

x is Element of the carrier of (T,([#] T),F)

j is Element of the carrier of T

UF is Element of F

[j,UF] is V35() set

{j,UF} is finite set

{j} is finite set

{{j,UF},{j}} is finite V45() set

x is set

A is Element of the carrier of T

[A,UF] is V35() set

{A,UF} is finite set

{A} is finite set

{{A,UF},{A}} is finite V45() set

B is Element of the carrier of (T,([#] T),F)

B `2 is set

B `1 is set

(T,([#] T),F) . B is Element of the carrier of T

the mapping of (T,([#] T),F) is non empty Relation-like the carrier of (T,([#] T),F) -defined the carrier of T -valued Function-like V38( the carrier of (T,([#] T),F), the carrier of T) Element of K10(K11( the carrier of (T,([#] T),F), the carrier of T))

K11( the carrier of (T,([#] T),F), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (T,([#] T),F), the carrier of T)) is non empty set

the mapping of (T,([#] T),F) . B is Element of the carrier of T

x `2 is set

T is non empty 1-sorted

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),F) is non empty reflexive transitive strict directed NetStr over T

(T,(T,([#] T),F)) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

F \ {{}} is Element of K10( the carrier of (BoolePoset ([#] T)))

T is non empty 1-sorted

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),F) is non empty reflexive transitive strict NetStr over T

x is non empty Element of K10( the carrier of T)

F \ {{}} is Element of K10( the carrier of (BoolePoset ([#] T)))

(T,(T,([#] T),F)) is non empty upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),F) is non empty reflexive transitive strict directed NetStr over T

(T,(T,([#] T),F)) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is Element of the carrier of T

x is Element of the carrier of T

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),F) is non empty reflexive transitive strict directed NetStr over T

Lim (T,([#] T),F) is Element of K10( the carrier of T)

(T,(T,([#] T),F)) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is Element of the carrier of T

x is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of the carrier of T

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is Element of K10( the carrier of T)

Cl x is closed Element of K10( the carrier of T)

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),x) is non empty reflexive transitive strict directed NetStr over T

the carrier of (T,([#] T),x) is non empty set

j is Element of the carrier of (T,([#] T),x)

{ [b

UF is Element of the carrier of T

x is Element of x

[UF,x] is V35() set

{UF,x} is finite set

{UF} is finite set

{{UF,x},{UF}} is finite V45() set

j `2 is set

A is a_neighborhood of F

B is set

C is Element of the carrier of T

[C,A] is V35() set

{C,A} is finite set

{C} is finite set

{{C,A},{C}} is finite V45() set

c is Element of the carrier of (T,([#] T),x)

(T,([#] T),x) . c is Element of the carrier of T

the mapping of (T,([#] T),x) is non empty Relation-like the carrier of (T,([#] T),x) -defined the carrier of T -valued Function-like V38( the carrier of (T,([#] T),x), the carrier of T) Element of K10(K11( the carrier of (T,([#] T),x), the carrier of T))

K11( the carrier of (T,([#] T),x), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (T,([#] T),x), the carrier of T)) is non empty set

the mapping of (T,([#] T),x) . c is Element of the carrier of T

c `1 is set

c `2 is set

T is non empty 1-sorted

F is set

x is non empty transitive directed NetStr over T

the carrier of x is non empty set

x is Element of the carrier of x

x is non empty transitive directed subnet of x

the carrier of x is non empty set

K11( the carrier of x, the carrier of x) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of x)) is non empty set

the carrier of T is non empty set

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V38( the carrier of x, the carrier of T) Element of K10(K11( the carrier of x, the carrier of T))

K11( the carrier of x, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of T)) is non empty set

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V38( the carrier of x, the carrier of T) Element of K10(K11( the carrier of x, the carrier of T))

K11( the carrier of x, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of T)) is non empty set

j is Relation-like the carrier of x -defined the carrier of x -valued Function-like V38( the carrier of x, the carrier of x) Element of K10(K11( the carrier of x, the carrier of x))

the mapping of x * j is Relation-like the carrier of x -defined the carrier of T -valued Function-like Element of K10(K11( the carrier of x, the carrier of T))

UF is Element of the carrier of x

x is Element of the carrier of x

x . x is Element of the carrier of T

the mapping of x . x is Element of the carrier of T

j . x is Element of the carrier of x

x . (j . x) is Element of the carrier of T

the mapping of x . (j . x) is Element of the carrier of T

T is non empty TopSpace-like TopStruct

F is set

x is set

x is set

the carrier of T is non empty set

K10( the carrier of T) is non empty set

x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is Element of the carrier of T

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

(T,x) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),x) is non empty reflexive transitive strict directed NetStr over T

(T,([#] T),x) " F is transitive strict full SubNetStr of (T,([#] T),x)

x is non empty transitive directed subnet of (T,([#] T),x)

j is non empty transitive directed NetStr over T

UF is non empty transitive directed NetStr over T

Lim (T,([#] T),x) is Element of K10( the carrier of T)

Lim x is Element of K10( the carrier of T)

x is non empty transitive directed NetStr over T

the carrier of x is non empty set

j is Element of the carrier of x

UF is Element of K10( the carrier of T)

Int UF is open Element of K10( the carrier of T)

x is Element of the carrier of x

x . x is Element of the carrier of T

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V38( the carrier of x, the carrier of T) Element of K10(K11( the carrier of x, the carrier of T))

K11( the carrier of x, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of T)) is non empty set

the mapping of x . x is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is Element of the carrier of T

x is non empty transitive directed NetStr over T

x is non empty transitive directed subnet of x

Lim x is Element of K10( the carrier of T)

j is non empty transitive directed convergent NetStr over T

UF is non empty transitive directed convergent NetStr over T

Lim UF is Element of K10( the carrier of T)

x is non empty transitive directed convergent NetStr over T

Lim x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is non empty transitive directed NetStr over T

x is Element of the carrier of T

x is set

x is Element of the carrier of T

x is non empty transitive directed NetStr over T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is non empty transitive directed convergent NetStr over T

x is Element of the carrier of T

Lim x is Element of K10( the carrier of T)

x is set

x is Element of the carrier of T

x is non empty transitive directed convergent NetStr over T

Lim x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is Element of the carrier of T

x is non empty transitive directed NetStr over T

(T,x) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

j is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),x) is non empty reflexive transitive strict directed NetStr over T

(T,(T,([#] T),x)) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is Element of the carrier of T

x is non empty transitive directed NetStr over T

x is non empty transitive directed subnet of x

Lim x is Element of K10( the carrier of T)

(T,x) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

UF is non empty filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

A is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

x is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is Element of the carrier of T

x is set

x is Element of the carrier of T

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

x is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

x is Element of the carrier of T

x is set

x is Element of the carrier of T

x is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

x is Element of the carrier of T

x is (T,F)

Cl x is closed Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

x is a_neighborhood of x

the carrier of F is non empty set

x is Element of the carrier of F

F | x is non empty transitive strict directed subnet of F

the mapping of (F | x) is non empty Relation-like the carrier of (F | x) -defined the carrier of T -valued Function-like V38( the carrier of (F | x), the carrier of T) Element of K10(K11( the carrier of (F | x), the carrier of T))

the carrier of (F | x) is non empty set

K11( the carrier of (F | x), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | x), the carrier of T)) is non empty set

rng the mapping of (F | x) is non empty Element of K10( the carrier of T)

j is (T,F)

Int x is open Element of K10( the carrier of T)

j /\ (Int x) is Element of K10( the carrier of T)

the Element of j /\ (Int x) is Element of j /\ (Int x)

Cl j is closed Element of K10( the carrier of T)

{} T is empty proper Relation-like non-empty empty-yielding finite finite-yielding V45() open closed boundary nowhere_dense Element of K10( the carrier of T)

dom the mapping of (F | x) is non empty Element of K10( the carrier of (F | x))

K10( the carrier of (F | x)) is non empty set

x is set

the mapping of (F | x) . x is set

{ b

A is Element of the carrier of (F | x)

B is Element of the carrier of F

F . B is Element of the carrier of T

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F . B is Element of the carrier of T

(F | x) . A is Element of the carrier of T

the mapping of (F | x) . A is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

FinMeetCl F is Element of K10(K10( the carrier of T))

x is Element of K10( the carrier of T)

x is Element of K10(K10( the carrier of T))

Intersect x is Element of K10( the carrier of T)

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

meet x is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

{ (Cl b

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

K10( the carrier of T) is non empty set

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

x is set

x is (T,F)

Cl x is closed Element of K10( the carrier of T)

x is Element of K10(K10( the carrier of T))

meet x is Element of K10( the carrier of T)

the Element of meet x is Element of meet x

the carrier of F is non empty set

the (T,F) is (T,F)

Cl the (T,F) is closed Element of K10( the carrier of T)

UF is set

meet UF is set

x is set

A is (T,F)

Cl A is closed Element of K10( the carrier of T)

B is Element of the carrier of F

F | B is non empty transitive strict directed subnet of F

the mapping of (F | B) is non empty Relation-like the carrier of (F | B) -defined the carrier of T -valued Function-like V38( the carrier of (F | B), the carrier of T) Element of K10(K11( the carrier of (F | B), the carrier of T))

the carrier of (F | B) is non empty set

K11( the carrier of (F | B), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | B), the carrier of T)) is non empty set

rng the mapping of (F | B) is non empty Element of K10( the carrier of T)

C is set

c is set

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

K10( the carrier of F) is non empty set

[#] F is non empty non proper lower upper Element of K10( the carrier of F)

A is finite Element of K10( the carrier of F)

B is Element of the carrier of F

C is set

x . C is set

c is (T,F)

Cl c is closed Element of K10( the carrier of T)

a is Element of the carrier of F

F | a is non empty transitive strict directed subnet of F

the mapping of (F | a) is non empty Relation-like the carrier of (F | a) -defined the carrier of T -valued Function-like V38( the carrier of (F | a), the carrier of T) Element of K10(K11( the carrier of (F | a), the carrier of T))

the carrier of (F | a) is non empty set

K11( the carrier of (F | a), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (F | a), the carrier of T)) is non empty set

rng the mapping of (F | a) is non empty Element of K10( the carrier of T)

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

the mapping of F | the carrier of (F | a) is Relation-like the carrier of F -defined the carrier of (F | a) -defined the carrier of F -defined the carrier of T -valued Function-like Element of K10(K11( the carrier of F, the carrier of T))

dom the mapping of (F | a) is non empty Element of K10( the carrier of (F | a))

K10( the carrier of (F | a)) is non empty set

the mapping of (F | a) . B is set

F . B is Element of the carrier of T

the mapping of F . B is Element of the carrier of T

j is Element of K10( the carrier of T)

UF is (T,F)

Cl UF is closed Element of K10( the carrier of T)

j is Element of the carrier of T

UF is (T,F)

Cl UF is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

NetUniv T is non empty set

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

x is Element of K10(K10( the carrier of T))

FinMeetCl x is Element of K10(K10( the carrier of T))

x is set

the Element of x is Element of x

UF is Element of K10(K10( the carrier of T))

Intersect UF is Element of K10( the carrier of T)

meet UF is Element of K10( the carrier of T)

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

j is non empty Element of K10(K10( the carrier of T))

InclPoset j is non empty strict reflexive transitive antisymmetric RelStr

(InclPoset j) ~ is non empty strict reflexive transitive antisymmetric RelStr

RelIncl j is Relation-like j -defined j -valued reflexive antisymmetric transitive V33(j) Element of K10(K11(j,j))

K11(j,j) is non empty Relation-like set

K10(K11(j,j)) is non empty set

RelStr(# j,(RelIncl j) #) is strict RelStr

the carrier of ((InclPoset j) ~) is non empty set

x is Element of the carrier of ((InclPoset j) ~)

[#] ((InclPoset j) ~) is non empty non proper lower upper Element of K10( the carrier of ((InclPoset j) ~))

K10( the carrier of ((InclPoset j) ~)) is non empty set

A is Element of the carrier of ((InclPoset j) ~)

~ x is Element of the carrier of (InclPoset j)

the carrier of (InclPoset j) is non empty set

B is Element of K10(K10( the carrier of T))

Intersect B is Element of K10( the carrier of T)

C is Element of K10(K10( the carrier of T))

Intersect C is Element of K10( the carrier of T)

C \/ B is Element of K10(K10( the carrier of T))

Intersect (C \/ B) is Element of K10( the carrier of T)

a is Element of the carrier of ((InclPoset j) ~)

~ a is Element of the carrier of (InclPoset j)

~ A is Element of the carrier of (InclPoset j)

x is non empty transitive directed RelStr

the carrier of x is non empty set

K11( the carrier of x, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of T)) is non empty set

A is Relation-like the carrier of x -defined the carrier of T -valued Function-like V38( the carrier of x, the carrier of T) Element of K10(K11( the carrier of x, the carrier of T))

x *' A is non empty transitive strict directed NetStr over T

the carrier of (x *' A) is non empty set

the InternalRel of (x *' A) is Relation-like the carrier of (x *' A) -defined the carrier of (x *' A) -valued Element of K10(K11( the carrier of (x *' A), the carrier of (x *' A)))

K11( the carrier of (x *' A), the carrier of (x *' A)) is non empty Relation-like set

K10(K11( the carrier of (x *' A), the carrier of (x *' A))) is non empty set

RelStr(# the carrier of (x *' A), the InternalRel of (x *' A) #) is strict RelStr

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K10(K11( the carrier of x, the carrier of x))

K11( the carrier of x, the carrier of x) is non empty Relation-like set

K10(K11( the carrier of x, the carrier of x)) is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the_universe_of the carrier of T is V9() Tarski set

the_transitive-closure_of the carrier of T is set

Tarski-Class (the_transitive-closure_of the carrier of T) is set

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

C is Element of the carrier of T

the mapping of (x *' A) is non empty Relation-like the carrier of (x *' A) -defined the carrier of T -valued Function-like V38( the carrier of (x *' A), the carrier of T) Element of K10(K11( the carrier of (x *' A), the carrier of T))

K11( the carrier of (x *' A), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of (x *' A), the carrier of T)) is non empty set

c is set

V is Element of K10( the carrier of T)

Int V is open Element of K10( the carrier of T)

a is Element of the carrier of (x *' A)

b is Element of the carrier of (x *' A)

(x *' A) . b is Element of the carrier of T

the mapping of (x *' A) . b is Element of the carrier of T

a9 is Element of the carrier of ((InclPoset j) ~)

b9 is Element of the carrier of ((InclPoset j) ~)

~ b9 is Element of the carrier of (InclPoset j)

the carrier of (InclPoset j) is non empty set

~ a9 is Element of the carrier of (InclPoset j)

a is Element of K10( the carrier of T)

Cl a is closed Element of K10( the carrier of T)

meet x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

x is non empty proper filtered upper ultra Element of K10( the carrier of (BoolePoset ([#] T)))

{ (Cl b

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

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

x is set

j is Element of K10( the carrier of T)

Cl j is closed Element of K10( the carrier of T)

x is Element of K10(K10( the carrier of T))

the Element of x is Element of x

UF is Element of K10( the carrier of T)

Cl UF is closed Element of K10( the carrier of T)

x is set

meet x is set

A is finite Element of K10(K10( the carrier of T))

B is set

C is Element of K10( the carrier of T)

Cl C is closed Element of K10( the carrier of T)

Intersect A is Element of K10( the carrier of T)

meet x is Element of K10( the carrier of T)

the Element of meet x is Element of meet x

UF is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

Cl x is closed Element of K10( the carrier of T)

UF is Element of the carrier of T

x is Element of the carrier of T

A is Element of K10( the carrier of T)

A ` is Element of K10( the carrier of T)

the carrier of T \ A is set

Cl (A `) is closed Element of K10( the carrier of T)

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

x is Element of K10(K10( the carrier of T))

the carrier of (BoolePoset the carrier of T) is non empty non trivial set

K10( the carrier of (BoolePoset the carrier of T)) is non empty set

x is Element of K10( the carrier of (BoolePoset the carrier of T))

fininfs x is non empty filtered Element of K10( the carrier of (BoolePoset the carrier of T))

K10(x) is non empty set

{ ("/\" (b

uparrow (fininfs x) is non empty filtered upper Element of K10( the carrier of (BoolePoset the carrier of T))

Bottom (BoolePoset the carrier of T) is Element of the carrier of (BoolePoset the carrier of T)

UF is Element of the carrier of (BoolePoset the carrier of T)

x is finite Element of K10(x)

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

Top (BoolePoset the carrier of T) is Element of the carrier of (BoolePoset the carrier of T)

A is Element of K10( the carrier of (BoolePoset the carrier of T))

meet A is set

UF is non empty filtered upper Element of K10( the carrier of (BoolePoset the carrier of T))

x is Element of the carrier of T

A is set

C is Element of K10( the carrier of T)

a is Element of the carrier of (BoolePoset the carrier of T)

c is Element of the carrier of (BoolePoset the carrier of T)

a "/\" c is Element of the carrier of (BoolePoset the carrier of T)

A /\ C is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

meet x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

BoolePoset ([#] T) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset ([#] T)) is non empty non trivial set

K10( the carrier of (BoolePoset ([#] T))) is non empty set

F is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

(T,([#] T),x) is non empty reflexive transitive strict directed NetStr over T

x is Element of the carrier of T

x is Element of the carrier of T

F is non empty transitive directed NetStr over T

NetUniv T is non empty set

BoolePoset the carrier of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V100() directed up-complete /\-complete V142() with_suprema with_infima V170() RelStr

the carrier of (BoolePoset the carrier of T) is non empty non trivial set

K10( the carrier of (BoolePoset the carrier of T)) is non empty set

(T,F) is non empty proper filtered upper Element of K10( the carrier of (BoolePoset ([#] T)))

{ b

x is non empty proper filtered upper Element of K10( the carrier of (BoolePoset the carrier of T))

x is Element of the carrier of T

x is Element of the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

F is non empty transitive directed NetStr over T

NetUniv T is non empty set

F is non empty transitive directed NetStr over T

T is non empty TopSpace-like TopStruct

F is non empty transitive directed NetStr over T

NetUniv T is non empty set

the carrier of T is non empty set

x is non empty TopSpace-like TopStruct

NetUniv x is non empty set

the carrier of x is non empty set

T is non empty 1-sorted

F is transitive NetStr over T

x is full SubNetStr of F

T is non empty 1-sorted

F is non empty directed NetStr over T

the carrier of F is non empty set

the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K10(K11( the carrier of F, the carrier of F))

K11( the carrier of F, the carrier of F) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of F)) is non empty set

the mapping of F is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V38( the carrier of F, the carrier of T) Element of K10(K11( the carrier of F, the carrier of T))

the carrier of T is non empty set

K11( the carrier of F, the carrier of T) is non empty Relation-like set

K10(K11( the carrier of F, the carrier of T)) is non empty set

NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) is non empty strict NetStr over T

RelStr(# the carrier of F, the InternalRel of F #) is strict RelStr

the mapping of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) is non empty Relation-like the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) -defined the carrier of T -valued Function-like V38( the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #), the carrier of T) Element of K10(K11( the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #), the carrier of T))

the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) is non empty set

K11( the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #), the carrier of T) is non empty Relation-like set

K10(K11( the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #), the carrier of T)) is non empty set

the mapping of F | the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) is Relation-like the carrier of F -defined the carrier of NetStr(# the carrier of F, the InternalRel of F, the mapping of F #) -defined the carrier of F -defined the carrier of T -valued Function-like Element of K10(K11( the carrier of F, the carrier of T))

[#] F is non empty non proper lower upper Element of K10( the carrier of F)

K10( the carrier of F) is non empty set

x is non empty