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
{ b1 where b1 is a_neighborhood of F : verum } is 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
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
{ b1 where b1 is a_neighborhood of F : verum } is set
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
{ b1 where b1 is a_neighborhood of F : verum } is set
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)))
{ b1 where b1 is a_neighborhood of F : verum } is set
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
{ b1 where b1 is a_neighborhood of F : verum } is set
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)))
{ b1 where b1 is a_neighborhood of x : verum } 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 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
{ b1 where b1 is Element of the carrier of F : j <= b1 } is set
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)
{ b1 where b1 is Element of the carrier of F : a <= b1 } is set
(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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
[#] 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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is 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
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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
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
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
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))
{ [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } is set
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( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T) is Relation-like set
K10(K11( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T)) is non empty set
x is Relation-like { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } -defined the carrier of T -valued Function-like V38( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T) Element of K10(K11( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T))
UF is Relation-like { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } -defined the carrier of T -valued Function-like V38( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T) Element of K10(K11( { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } , the carrier of T))
A is set
x . A is set
UF . A is set
c is Element of { [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 }
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
{ [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),F) is_eventually_in b1 } is set
the carrier of (T,([#] T),F) is non empty set
{ [b1,b2] where b1 is Element of the carrier of T, b2 is Element of F : b1 in b2 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),F) is_eventually_in b1 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),F) is_eventually_in b1 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),F) is_eventually_in b1 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),F) is_eventually_in b1 } is set
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)))
{ b1 where b1 is a_neighborhood of F : verum } is set
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)
{ [b1,b2] where b1 is Element of the carrier of T, b2 is Element of x : b1 in b2 } is set
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)))
{ b1 where b1 is a_neighborhood of x : verum } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : x is_eventually_in b1 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : (T,([#] T),x) is_eventually_in b1 } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : x is_eventually_in b1 } is set
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
{ b1 where b1 is Element of the carrier of F : x <= b1 } is set
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 b1) where b1 is (T,F) : verum } is set
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 b1) where b1 is Element of K10( the carrier of T) : b1 in x } is 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)
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
{ ("/\" (b1,(BoolePoset the carrier of T))) where b1 is finite Element of K10(x) : ex_inf_of b1, BoolePoset the carrier of T } is set
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)))
{ b1 where b1 is Element of K10( the carrier of T) : F is_eventually_in b1 } is set
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 strict full SubNetStr of F
[#] x is non empty non proper lower upper Element of K10( the carrier of x)
the carrier of x is non empty set
K10( the carrier of x) is non empty set
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 non empty transitive directed subnet of F
Lim x is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x is non empty transitive directed subnet of F
F is non empty transitive directed NetStr over T
x is non empty transitive directed subnet of F
Lim x is Element of K10( the carrier of T)
the Element of Lim x is Element of Lim x
x is Element of the carrier of T
j is Element of the carrier of T
T is non empty 1-sorted
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 ultra Element of K10( the carrier of (BoolePoset ([#] T)))
(T,([#] T),F) is non empty reflexive transitive strict directed NetStr over T
x is Element of K10( the carrier of T)
x ` is Element of K10( the carrier of T)
the carrier of T \ x is set
{} T is empty proper Relation-like non-empty empty-yielding finite finite-yielding V45() Element of K10( the carrier of T)
({} T) ` is Element of K10( the carrier of T)
the carrier of T \ ({} T) is set
T is non empty TopSpace-like TopStruct
F is non empty transitive directed NetStr over T
the carrier of T is non empty set
K10( the carrier of T) is non empty set
x is Element of the carrier of T
x is a_neighborhood of x
x ` is Element of K10( the carrier of T)
the carrier of T \ x is set
the carrier of F is non empty set
x is Element of the carrier of F
j is Element of the carrier of F
F . j 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 . j is Element of the carrier of T
Lim F 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)
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 ultra Element of K10( the carrier of (BoolePoset ([#] T)))
(T,([#] T),F) is non empty reflexive transitive strict directed (T) NetStr over T
Lim (T,([#] T),F) is Element of K10( the carrier of T)
the Element of Lim (T,([#] T),F) is Element of Lim (T,([#] T),F)
x is Element of the carrier of T
x is Element of the carrier of T