:: WAYBEL33 semantic presentation

K130() is non trivial V11() non finite cardinal limit_cardinal Element of bool K126()
K126() is set
bool K126() is non empty set
K37() is non trivial V11() non finite cardinal limit_cardinal set
bool K37() is non empty non trivial non finite set
bool K130() is non empty non trivial non finite set
2 is non empty set
[:2,2:] is non empty Relation-like set
[:[:2,2:],2:] is non empty Relation-like set
bool [:[:2,2:],2:] is non empty set
{} is set
the empty Relation-like non-empty empty-yielding V11() V15() finite finite-yielding V50() cardinal {} -element set is empty Relation-like non-empty empty-yielding V11() V15() finite finite-yielding V50() cardinal {} -element set
1 is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T is non empty Element of bool the carrier of L
BoolePoset T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset T) is non empty non trivial set
bool the carrier of (BoolePoset T) is non empty set
x is non empty filtered upper Element of bool the carrier of (BoolePoset T)
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in x } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in x } ,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
bool the carrier of L is non empty set
bool the carrier of T is non empty set
x is non empty Element of bool the carrier of L
BoolePoset x is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset x) is non empty non trivial set
bool the carrier of (BoolePoset x) is non empty set
y is non empty Element of bool the carrier of T
BoolePoset y is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset y) is non empty non trivial set
bool the carrier of (BoolePoset y) is non empty set
z is non empty filtered upper Element of bool the carrier of (BoolePoset x)
(L,x,z) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in z } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in z } ,L) is Element of the carrier of L
x is non empty filtered upper Element of bool the carrier of (BoolePoset y)
(T,y,x) is Element of the carrier of T
{ ("/\" (b₁,T)) where b₁ is Element of bool the carrier of T : b₁ in x } is set
"\/" ( { ("/\" (b₁,T)) where b₁ is Element of bool the carrier of T : b₁ in x } ,T) is Element of the carrier of T
F is set
a is Element of bool the carrier of T
"/\" (a,T) is Element of the carrier of T
bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
j2 is Element of bool the carrier of L
"/\" (j2,L) is Element of the carrier of L
F is set
a is Element of bool the carrier of L
"/\" (a,L) is Element of the carrier of L
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty set
j2 is Element of bool the carrier of T
"/\" (j2,T) is Element of the carrier of T
L is non empty TopRelStr
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
xi L is Element of bool (bool the carrier of L)
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set
x is Element of bool (bool the carrier of L)
union x is Element of bool the carrier of L
y is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
union y is Element of bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))
x is Element of bool the carrier of L
y is Element of bool the carrier of L
x /\ y is Element of bool the carrier of L
L is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr
the carrier of L is non empty set
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
T is non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact TopRelStr
the carrier of T is non empty trivial finite 1 -element set
the Element of the carrier of T is Element of the carrier of T
x is non empty trivial finite 1 -element TopSpace-like compact TopStruct
the carrier of x is non empty trivial finite 1 -element set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
z is Element of the carrier of x
{z} is non empty trivial finite 1 -element Element of bool the carrier of x
bool the carrier of x is non empty finite V50() set
{{},{z}} is finite set
the topology of x is finite V50() Element of bool (bool the carrier of x)
bool (bool the carrier of x) is non empty finite V50() set
xi L is Element of bool (bool the carrier of L)
the non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact () TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact () TopRelStr
L is non empty 1-sorted
the carrier of L is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
x is NetStr over L
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
bool [: 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 mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
[: the carrier of x, the carrier of T:] is Relation-like set
bool [: the carrier of x, the carrier of T:] is non empty set
y is Relation-like the carrier of x -defined the carrier of T -valued Function-like V41( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
NetStr(# the carrier of x, the InternalRel of x,y #) is strict NetStr over T
the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) is set
the InternalRel of NetStr(# the carrier of x, the InternalRel of x,y #) is Relation-like the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -defined the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -valued Element of bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):]
[: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):] is Relation-like set
bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):] is non empty set
RelStr(# the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the InternalRel of NetStr(# the carrier of x, the InternalRel of x,y #) #) is strict RelStr
the mapping of NetStr(# the carrier of x, the InternalRel of x,y #) is Relation-like the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -defined the carrier of T -valued Function-like V41( the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T) Element of bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:]
[: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:] is Relation-like set
bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:] is non empty set
L is non empty 1-sorted
the carrier of L is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
NetUniv L is non empty set
NetUniv T is non empty set
x is NetStr over L
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
bool [: 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 mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski universal set
y is non empty transitive strict directed NetStr over L
the carrier of y is non empty set
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of L -valued Function-like V41( the carrier of y, the carrier of L) Element of bool [: the carrier of y, the carrier of L:]
[: the carrier of y, the carrier of L:] is non empty Relation-like set
bool [: the carrier of y, the carrier of L:] is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
z is Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
NetStr(# the carrier of y, the InternalRel of y,z #) is non empty transitive strict directed NetStr over T
the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) is non empty set
the InternalRel of NetStr(# the carrier of y, the InternalRel of y,z #) is Relation-like the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -defined the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -valued Element of bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):]
[: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):] is non empty Relation-like set
bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):] is non empty set
RelStr(# the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the InternalRel of NetStr(# the carrier of y, the InternalRel of y,z #) #) is strict RelStr
the mapping of NetStr(# the carrier of y, the InternalRel of y,z #) is non empty Relation-like the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -defined the carrier of T -valued Function-like V41( the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T) Element of bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:]
[: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:] is non empty Relation-like set
bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:] is non empty set
L is non empty RelStr
T is non empty RelStr
x is non empty transitive directed NetStr over L
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
y is non empty transitive directed NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the carrier of L 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 L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is non empty Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
{ (y . b₁) where b₁ is Element of the carrier of y : a₁ <= b₁ } is set
{ (x . b₁) where b₁ is Element of the carrier of x : a₁ <= b₁ } is set
z is Element of the carrier of x
x is Element of the carrier of y
{ (x . b₁) where b₁ is Element of the carrier of x : z <= b₁ } is set
{ (y . b₁) where b₁ is Element of the carrier of y : x <= b₁ } is set
y is set
A is Element of the carrier of x
x . A is Element of the carrier of L
the mapping of x . A is Element of the carrier of L
F is Element of the carrier of x
x . F is Element of the carrier of L
the mapping of x . F is Element of the carrier of L
a is Element of the carrier of y
y . a is Element of the carrier of T
the mapping of y . a is Element of the carrier of T
j2 is Element of the carrier of y
L is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty transitive directed NetStr over L
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
y is non empty transitive directed NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is non empty Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
{ (y . b₁) where b₁ is Element of the carrier of y : a₁ <= b₁ } is set
{ (x . b₁) where b₁ is Element of the carrier of x : a₁ <= b₁ } is set
{ ("/\" (H₂(b₁),L)) where b₁ is Element of the carrier of x : verum } is set
{ ("/\" (H₁(b₁),T)) where b₁ is Element of the carrier of y : verum } is set
y is set
A is Element of the carrier of x
{ (x . b₁) where b₁ is Element of the carrier of x : A <= b₁ } is set
"/\" (H₂(A),L) is Element of the carrier of L
F is Element of the carrier of y
{ (y . b₁) where b₁ is Element of the carrier of y : F <= b₁ } is set
a is Element of the carrier of x
{ (x . b₁) where b₁ is Element of the carrier of x : a <= b₁ } is set
j2 is set
G is Element of the carrier of x
x . G is Element of the carrier of L
the mapping of x . G is Element of the carrier of L
[#] x is non empty non proper lower upper Element of bool the carrier of x
bool the carrier of x is non empty set
j2 is Element of the carrier of x
x . j2 is Element of the carrier of L
the mapping of x . j2 is Element of the carrier of L
bool the carrier of L is non empty set
G is non empty Element of bool the carrier of L
"/\" (H₁(F),T) is Element of the carrier of T
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
x is non empty transitive directed NetStr over L
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: 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 mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is non empty Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
lim_inf x is Element of the carrier of L
y is non empty transitive directed NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
lim_inf y is Element of the carrier of T
{ (y . b₁) where b₁ is Element of the carrier of y : a₁ <= b₁ } is set
{ (x . b₁) where b₁ is Element of the carrier of x : a₁ <= b₁ } is set
{ ("/\" (H₂(b₁),L)) where b₁ is Element of the carrier of x : verum } is set
{ ("/\" (H₁(b₁),T)) where b₁ is Element of the carrier of y : verum } is set
"\/" ( { ("/\" (H₂(b₁),L)) where b₁ is Element of the carrier of x : verum } ,L) is Element of the carrier of L
"\/" ( { ("/\" (H₁(b₁),T)) where b₁ is Element of the carrier of y : verum } ,T) is Element of the carrier of T
y is set
A is Element of the carrier of x
{ (x . b₁) where b₁ is Element of the carrier of x : A <= b₁ } is set
"/\" ( { (x . b₁) where b₁ is Element of the carrier of x : A <= b₁ } ,L) is Element of the carrier of L
bool the carrier of L is non empty set
y is Element of bool the carrier of L
L is non empty 1-sorted
the carrier of L is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
x is non empty transitive directed NetStr over L
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: 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 mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is non empty Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
y is non empty transitive directed NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
z is non empty transitive directed subnet of x
the carrier of z is non empty set
the InternalRel of z is Relation-like the carrier of z -defined the carrier of z -valued Element of bool [: the carrier of z, the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty Relation-like set
bool [: the carrier of z, the carrier of z:] is non empty set
RelStr(# the carrier of z, the InternalRel of z #) is strict RelStr
the mapping of z is non empty Relation-like the carrier of z -defined the carrier of L -valued Function-like V41( the carrier of z, the carrier of L) Element of bool [: the carrier of z, the carrier of L:]
[: the carrier of z, the carrier of L:] is non empty Relation-like set
bool [: the carrier of z, the carrier of L:] is non empty set
x is strict NetStr over T
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
bool [: 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 mapping of x is Relation-like the carrier of x -defined the carrier of T -valued Function-like V41( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
[: the carrier of x, the carrier of T:] is Relation-like set
bool [: the carrier of x, the carrier of T:] is non empty set
[: the carrier of z, the carrier of x:] is non empty Relation-like set
bool [: the carrier of z, the carrier of x:] is non empty set
A is Relation-like the carrier of z -defined the carrier of x -valued Function-like V41( the carrier of z, the carrier of x) Element of bool [: the carrier of z, the carrier of x:]
the mapping of x * A is Relation-like the carrier of z -defined the carrier of L -valued Function-like Element of bool [: the carrier of z, the carrier of L:]
y is non empty transitive strict directed NetStr over T
the carrier of y is non empty set
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
F is Relation-like the carrier of y -defined the carrier of y -valued Function-like V41( the carrier of y, the carrier of y) Element of bool [: the carrier of y, the carrier of y:]
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
the mapping of y * F is Relation-like the carrier of y -defined the carrier of T -valued Function-like Element of bool [: the carrier of y, the carrier of T:]
a is Element of the carrier of y
j2 is Element of the carrier of x
G is Element of the carrier of z
g is Element of the carrier of y
G is Element of the carrier of y
F . G is Element of the carrier of y
F is Element of the carrier of z
A . F is Element of the carrier of x
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
lim_inf-Convergence L is Relation-like Convergence-Class of L
lim_inf-Convergence T is Relation-like Convergence-Class of T
x is NetStr over L
the carrier of x is set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
bool [: 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 mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
y is set
[x,y] is V38() set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V50() set
NetUniv L is non empty set
[:(NetUniv L), the carrier of L:] is non empty Relation-like set
z is set
x is set
[z,x] is V38() set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V50() set
NetUniv T is non empty set
A is non empty transitive strict directed NetStr over T
the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of T -valued Function-like V41( the carrier of A, the carrier of T) Element of bool [: the carrier of A, the carrier of T:]
[: the carrier of A, the carrier of T:] is non empty Relation-like set
bool [: the carrier of A, the carrier of T:] is non empty set
the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski universal set
a is non empty transitive strict directed NetStr over L
the carrier of a is non empty set
F is non empty transitive strict directed NetStr over L
a is non empty transitive directed subnet of A
the carrier of a is non empty set
the InternalRel of a is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty Relation-like set
bool [: the carrier of a, the carrier of a:] is non empty set
RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr
the mapping of a is non empty Relation-like the carrier of a -defined the carrier of T -valued Function-like V41( the carrier of a, the carrier of T) Element of bool [: the carrier of a, the carrier of T:]
[: the carrier of a, the carrier of T:] is non empty Relation-like set
bool [: the carrier of a, the carrier of T:] is non empty set
j2 is non empty transitive strict directed subnet of F
the carrier of j2 is non empty set
the InternalRel of j2 is Relation-like the carrier of j2 -defined the carrier of j2 -valued Element of bool [: the carrier of j2, the carrier of j2:]
[: the carrier of j2, the carrier of j2:] is non empty Relation-like set
bool [: the carrier of j2, the carrier of j2:] is non empty set
RelStr(# the carrier of j2, the InternalRel of j2 #) is strict RelStr
the mapping of j2 is non empty Relation-like the carrier of j2 -defined the carrier of L -valued Function-like V41( the carrier of j2, the carrier of L) Element of bool [: the carrier of j2, the carrier of L:]
[: the carrier of j2, the carrier of L:] is non empty Relation-like set
bool [: the carrier of j2, the carrier of L:] is non empty set
y is Element of the carrier of L
lim_inf j2 is Element of the carrier of L
lim_inf a is Element of the carrier of T
[A,y] is V38() set
{A,y} is finite set
{A} is non empty trivial finite 1 -element set
{{A,y},{A}} is finite V50() set
L is non empty 1-sorted
T is non empty 1-sorted
the carrier of L is non empty set
the carrier of T is non empty set
x is non empty NetStr over L
the carrier of x is non empty set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: 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 mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]
[: the carrier of x, the carrier of L:] is non empty Relation-like set
bool [: the carrier of x, the carrier of L:] is non empty set
y is non empty NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
z is set
x is Element of the carrier of x
y is Element of the carrier of y
A is Element of the carrier of y
y . A is Element of the carrier of T
the mapping of y . A is Element of the carrier of T
F is Element of the carrier of x
x . F is Element of the carrier of L
the mapping of x . F is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set
lim_inf-Convergence T is Relation-like Convergence-Class of T
ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))
the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set
x is set
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : for b₂ being Element of the carrier of T holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over T holds
( not [b₃,b₂] in lim_inf-Convergence T or b₃ is_eventually_in b₁ ) ) } is set
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of bool the carrier of L : for b₂ being Element of the carrier of L holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over L holds
( not [b₃,b₂] in lim_inf-Convergence L or b₃ is_eventually_in b₁ ) ) } is set
y is Element of bool the carrier of L
x is Element of the carrier of T
z is Element of bool the carrier of T
y is non empty transitive directed NetStr over T
[y,x] is V38() set
{y,x} is finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is finite V50() set
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is non empty Relation-like set
bool [: the carrier of y, the carrier of T:] is non empty set
A is non empty transitive strict directed NetStr over L
[A,x] is V38() set
{A,x} is finite set
{A} is non empty trivial finite 1 -element set
{{A,x},{A}} is finite V50() set
the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V41( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
[: the carrier of A, the carrier of L:] is non empty Relation-like set
bool [: the carrier of A, the carrier of L:] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
lim_inf-Convergence T is Relation-like Convergence-Class of T
ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set
the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))
the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
xi L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
xi T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set
lim_inf-Convergence T is Relation-like Convergence-Class of T
ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))
the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set
L is non empty reflexive lower-bounded /\-complete RelStr
T is non empty reflexive lower-bounded TopAugmentation of L
the carrier of T is non empty set
bool the carrier of T is non empty set
x is non empty Element of bool the carrier of T
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
bool the carrier of L is non empty set
y is non empty Element of bool the carrier of L
z is Element of the carrier of L
x is Element of the carrier of T
y is Element of the carrier of T
A is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
T is non empty reflexive transitive antisymmetric TopAugmentation of L
the carrier of T is non empty set
x is Element of the carrier of T
y is Element of the carrier of T
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
z is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
A is Element of the carrier of T
F is Element of the carrier of T
a is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
xi L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty strict TopRelStr
the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty set
the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):]
[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty Relation-like set
bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) is strict RelStr
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima TopAugmentation of L
the topology of x is Element of bool (bool the carrier of x)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
xi x is Element of bool (bool the carrier of x)
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
xi L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima () TopAugmentation of L
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
xi T is Element of bool (bool the carrier of T)
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L
x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
xi T is Element of bool (bool the carrier of T)
the topology of x is Element of bool (bool the carrier of x)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
xi x is Element of bool (bool the carrier of x)
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: 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 carrier of L is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
xi L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty strict TopRelStr
the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty set
the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is Relation-like the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) -defined the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):]
[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty Relation-like set
bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) is strict RelStr
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L
the topology of x is Element of bool (bool the carrier of x)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
xi x is Element of bool (bool the carrier of x)
L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr
(L) is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
T is non empty transitive directed NetStr over L
lim_inf T is Element of the carrier of L
the carrier of L is non empty set
the carrier of T is non empty set
{ (inf (T | b₁)) where b₁ is Element of the carrier of T : verum } is set
"\/" ( { (inf (T | b₁)) where b₁ is Element of the carrier of T : verum } ,L) is Element of the carrier of L
{ ("/\" ( { (T . b₂) where b₂ is Element of the carrier of T : b₁ <= b₂ } ,L)) where b₁ is Element of the carrier of T : verum } is set
z is set
x is Element of the carrier of T
{ (T . b₁) where b₁ is Element of the carrier of T : x <= b₁ } is set
"/\" ( { (T . b₁) where b₁ is Element of the carrier of T : x <= b₁ } ,L) is Element of the carrier of L
F is Element of the carrier of T
T | F is non empty transitive strict directed subnet of T
the mapping of (T | F) is non empty Relation-like the carrier of (T | F) -defined the carrier of L -valued Function-like V41( the carrier of (T | F), the carrier of L) Element of bool [: the carrier of (T | F), the carrier of L:]
the carrier of (T | F) is non empty set
[: the carrier of (T | F), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (T | F), the carrier of L:] is non empty set
rng the mapping of (T | F) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
a is set
{ ((T | F) . b₁) where b₁ is Element of the carrier of (T | F) : verum } is set
j2 is Element of the carrier of (T | F)
(T | F) . j2 is Element of the carrier of L
the mapping of (T | F) . j2 is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of T : F <= b₁ } is set
G is Element of the carrier of T
T . G is Element of the carrier of L
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
[: the carrier of T, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T, the carrier of L:] is non empty set
the mapping of T . G is Element of the carrier of L
g is Element of the carrier of (T | F)
(T | F) . g is Element of the carrier of L
the mapping of (T | F) . g is Element of the carrier of L
G is Element of the carrier of T
y is Element of the carrier of L
a is Element of the carrier of L
a is set
j2 is Element of the carrier of T
T . j2 is Element of the carrier of L
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
[: the carrier of T, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T, the carrier of L:] is non empty set
the mapping of T . j2 is Element of the carrier of L
G is Element of the carrier of T
{ b₁ where b₁ is Element of the carrier of T : F <= b₁ } is set
g is Element of the carrier of (T | F)
T . G is Element of the carrier of L
the mapping of T . G is Element of the carrier of L
G is Element of the carrier of (T | F)
(T | F) . G is Element of the carrier of L
the mapping of (T | F) . G is Element of the carrier of L
{ ((T | F) . b₁) where b₁ is Element of the carrier of (T | F) : verum } is set
a is Element of the carrier of L
a is Element of the carrier of T
T | a is non empty transitive strict directed subnet of T
the mapping of (T | a) is non empty Relation-like the carrier of (T | a) -defined the carrier of L -valued Function-like V41( the carrier of (T | a), the carrier of L) Element of bool [: the carrier of (T | a), the carrier of L:]
the carrier of (T | a) is non empty set
[: the carrier of (T | a), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (T | a), the carrier of L:] is non empty set
rng the mapping of (T | a) is non empty Element of bool the carrier of L
inf (T | a) is Element of the carrier of L
//\ ( the mapping of (T | a),L) is Element of the carrier of L
"/\" ((rng the mapping of (T | a)),L) is Element of the carrier of L
"\/" ( { ("/\" ( { (T . b₂) where b₂ is Element of the carrier of T : b₁ <= b₂ } ,L)) where b₁ is Element of the carrier of T : verum } ,L) is Element of the carrier of L
z is set
x is Element of the carrier of T
T | x is non empty transitive strict directed subnet of T
inf (T | x) is Element of the carrier of L
{ (T . b₁) where b₁ is Element of the carrier of T : x <= b₁ } is set
the mapping of (T | x) is non empty Relation-like the carrier of (T | x) -defined the carrier of L -valued Function-like V41( the carrier of (T | x), the carrier of L) Element of bool [: the carrier of (T | x), the carrier of L:]
the carrier of (T | x) is non empty set
[: the carrier of (T | x), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (T | x), the carrier of L:] is non empty set
rng the mapping of (T | x) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
A is set
{ ((T | x) . b₁) where b₁ is Element of the carrier of (T | x) : verum } is set
F is Element of the carrier of (T | x)
(T | x) . F is Element of the carrier of L
the mapping of (T | x) . F is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of T : x <= b₁ } is set
a is Element of the carrier of T
T . a is Element of the carrier of L
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
[: the carrier of T, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T, the carrier of L:] is non empty set
the mapping of T . a is Element of the carrier of L
j2 is Element of the carrier of (T | x)
(T | x) . j2 is Element of the carrier of L
the mapping of (T | x) . j2 is Element of the carrier of L
G is Element of the carrier of T
A is Element of the carrier of L
//\ ( the mapping of (T | x),L) is Element of the carrier of L
"/\" ((rng the mapping of (T | x)),L) is Element of the carrier of L
F is set
a is Element of the carrier of T
T . a is Element of the carrier of L
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
[: the carrier of T, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T, the carrier of L:] is non empty set
the mapping of T . a is Element of the carrier of L
j2 is Element of the carrier of T
{ b₁ where b₁ is Element of the carrier of T : x <= b₁ } is set
G is Element of the carrier of (T | x)
T . j2 is Element of the carrier of L
the mapping of T . j2 is Element of the carrier of L
g is Element of the carrier of (T | x)
(T | x) . g is Element of the carrier of L
the mapping of (T | x) . g is Element of the carrier of L
{ ((T | x) . b₁) where b₁ is Element of the carrier of (T | x) : verum } is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))
a_net T is non empty reflexive transitive strict directed NetStr over L
the carrier of (a_net T) is non empty set
x is Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
y is Element of the carrier of (a_net T)
y `2 is set
(a_net T) | y is non empty reflexive transitive strict directed subnet of a_net T
inf ((a_net T) | y) is Element of the carrier of L
the mapping of ((a_net T) | y) is non empty Relation-like the carrier of ((a_net T) | y) -defined the carrier of L -valued Function-like V41( the carrier of ((a_net T) | y), the carrier of L) Element of bool [: the carrier of ((a_net T) | y), the carrier of L:]
the carrier of ((a_net T) | y) is non empty set
[: the carrier of ((a_net T) | y), the carrier of L:] is non empty Relation-like set
bool [: the carrier of ((a_net T) | y), the carrier of L:] is non empty set
rng the mapping of ((a_net T) | y) is non empty Element of bool the carrier of L
z is set
x is Element of the carrier of L
y is Element of T
[x,y] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V50() set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of the carrier of L, b<sub>2</sub> is Element of T : b<sub>1</sub> in b<sub>2</sub> } is set
A is Element of the carrier of (a_net T)
[x,y] `1 is Element of the carrier of L
(a_net T) . A is Element of the carrier of L
the mapping of (a_net T) is non empty Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like V41( the carrier of (a_net T), the carrier of L) Element of bool [: the carrier of (a_net T), the carrier of L:]
[: the carrier of (a_net T), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (a_net T), the carrier of L:] is non empty set
the mapping of (a_net T) . A is Element of the carrier of L
[x,y] `2 is Element of T
A `2 is set
F is Element of the carrier of (a_net T)
{ b₁ where b₁ is Element of the carrier of (a_net T) : y <= b₁ } is set
a is Element of the carrier of ((a_net T) | y)
(a_net T) . F is Element of the carrier of L
the mapping of (a_net T) . F is Element of the carrier of L
j2 is Element of the carrier of ((a_net T) | y)
((a_net T) | y) . j2 is Element of the carrier of L
the mapping of ((a_net T) | y) . j2 is Element of the carrier of L
{ (((a_net T) | y) . b₁) where b₁ is Element of the carrier of ((a_net T) | y) : verum } is set
z is set
{ (((a_net T) | y) . b₁) where b₁ is Element of the carrier of ((a_net T) | y) : verum } is set
x is Element of the carrier of ((a_net T) | y)
((a_net T) | y) . x is Element of the carrier of L
the mapping of ((a_net T) | y) . x is Element of the carrier of L
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of T : b₁ in b₂ } is set
{ b₁ where b₁ is Element of the carrier of (a_net T) : y <= b₁ } is set
y is Element of the carrier of (a_net T)
y `2 is set
A is Element of the carrier of (a_net T)
A is Element of the carrier of L
F is Element of T
[A,F] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{A,F} is finite set
{A} is non empty trivial finite 1 -element set
{{A,F},{A}} is finite V50() set
[A,F] `1 is Element of the carrier of L
[A,F] `2 is Element of T
(a_net T) . y is Element of the carrier of L
the mapping of (a_net T) is non empty Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like V41( the carrier of (a_net T), the carrier of L) Element of bool [: the carrier of (a_net T), the carrier of L:]
[: the carrier of (a_net T), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (a_net T), the carrier of L:] is non empty set
the mapping of (a_net T) . y is Element of the carrier of L
a is Element of the carrier of ((a_net T) | y)
((a_net T) | y) . a is Element of the carrier of L
the mapping of ((a_net T) | y) . a is Element of the carrier of L
y `1 is set
//\ ( the mapping of ((a_net T) | y),L) is Element of the carrier of L
"/\" ((rng the mapping of ((a_net T) | y)),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))
(L,([#] L),T) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } ,L) is Element of the carrier of L
a_net T is non empty reflexive transitive strict directed NetStr over L
lim_inf (a_net T) is Element of the carrier of L
the carrier of (a_net T) is non empty set
{ (inf ((a_net T) | b₁)) where b₁ is Element of the carrier of (a_net T) : verum } is set
z is set
x is Element of the carrier of (a_net T)
(a_net T) | x is non empty reflexive transitive strict directed subnet of a_net T
inf ((a_net T) | x) is Element of the carrier of L
y is Element of the carrier of (a_net T)
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of T : b₁ in b₂ } is set
A is Element of the carrier of L
F is Element of T
[A,F] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{A,F} is finite set
{A} is non empty trivial finite 1 -element set
{{A,F},{A}} is finite V50() set
j2 is Element of the carrier of (BoolePoset ([#] L))
G is Element of bool the carrier of L
[A,G] is V38() Element of [: the carrier of L,(bool the carrier of L):]
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
{A,G} is finite set
{{A,G},{A}} is finite V50() set
[A,G] `2 is Element of bool the carrier of L
"/\" (G,L) is Element of the carrier of L
a is Element of the carrier of (a_net T)
(a_net T) | a is non empty reflexive transitive strict directed subnet of a_net T
inf ((a_net T) | a) is Element of the carrier of L
z is set
x is Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
Bottom (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))
y is Element of the carrier of L
A is Element of T
[y,A] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{y,A} is finite set
{y} is non empty trivial finite 1 -element set
{{y,A},{y}} is finite V50() set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of the carrier of L, b<sub>2</sub> is Element of T : b<sub>1</sub> in b<sub>2</sub> } is set
[y,A] `2 is Element of T
F is Element of the carrier of (a_net T)
(a_net T) | F is non empty reflexive transitive strict directed subnet of a_net T
inf ((a_net T) | F) is Element of the carrier of L
"\/" ( { (inf ((a_net T) | b₁)) where b₁ is Element of the carrier of (a_net T) : verum } ,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
T is non empty Element of bool the carrier of (BoolePoset ([#] L))
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of T : b₁ in b₂ } is set
x is set
y is Element of the carrier of L
z is Element of T
[y,z] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{y,z} is finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is finite V50() set
bool ([#] L) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
NetUniv L is non empty set
T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))
a_net T is non empty reflexive transitive strict directed NetStr over L
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of T : b₁ in b₂ } is set
the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski universal set
z is V9() subset-closed Tarski universal set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
the carrier of (a_net T) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))
a_net T is non empty reflexive transitive strict directed V266(L) NetStr over L
the carrier of (a_net T) is non empty set
[: the carrier of (a_net T), the carrier of (a_net T):] is non empty Relation-like set
bool [: the carrier of (a_net T), the carrier of (a_net T):] is non empty set
(L,([#] L),T) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } ,L) is Element of the carrier of L
x is Relation-like the carrier of (a_net T) -defined the carrier of (a_net T) -valued Function-like V41( the carrier of (a_net T), the carrier of (a_net T)) greater_or_equal_to_id Element of bool [: the carrier of (a_net T), the carrier of (a_net T):]
(a_net T) * x is non empty transitive strict directed subnet of a_net T
inf ((a_net T) * x) is Element of the carrier of L
the mapping of ((a_net T) * x) is non empty Relation-like the carrier of ((a_net T) * x) -defined the carrier of L -valued Function-like V41( the carrier of ((a_net T) * x), the carrier of L) Element of bool [: the carrier of ((a_net T) * x), the carrier of L:]
the carrier of ((a_net T) * x) is non empty set
[: the carrier of ((a_net T) * x), the carrier of L:] is non empty Relation-like set
bool [: the carrier of ((a_net T) * x), the carrier of L:] is non empty set
rng the mapping of ((a_net T) * x) is non empty Element of bool the carrier of L
the Element of T is Element of T
//\ ( the mapping of ((a_net T) * x),L) is Element of the carrier of L
"/\" ((rng the mapping of ((a_net T) * x)),L) is Element of the carrier of L
bool ([#] L) is non empty Element of bool (bool ([#] L))
bool ([#] L) is non empty set
bool (bool ([#] L)) is non empty set
the Element of T \ (rng the mapping of ((a_net T) * x)) is Element of bool the Element of T
bool the Element of T is non empty set
the Element of T /\ (rng the mapping of ((a_net T) * x)) is Element of bool the carrier of L
[: the carrier of ((a_net T) * x), the carrier of (a_net T):] is non empty Relation-like set
bool [: the carrier of ((a_net T) * x), the carrier of (a_net T):] is non empty set
y is Element of the carrier of (BoolePoset ([#] L))
the Element of y is Element of y
Bottom (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))
G is Element of the carrier of L
j2 is Element of T
[G,j2] is V38() Element of [: the carrier of L,T:]
[: the carrier of L,T:] is non empty Relation-like set
{G,j2} is finite set
{G} is non empty trivial finite 1 -element set
{{G,j2},{G}} is finite V50() set
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of T : b₁ in b₂ } is set
g is Element of the carrier of (a_net T)
dom x is Element of bool the carrier of (a_net T)
bool the carrier of (a_net T) is non empty set
F is Relation-like the carrier of ((a_net T) * x) -defined the carrier of (a_net T) -valued Function-like V41( the carrier of ((a_net T) * x), the carrier of (a_net T)) Element of bool [: the carrier of ((a_net T) * x), the carrier of (a_net T):]
G is Element of the carrier of ((a_net T) * x)
F is Element of the carrier of ((a_net T) * x)
f0 is Element of the carrier of ((a_net T) * x)
F . f0 is Element of the carrier of (a_net T)
p is Element of the carrier of (a_net T)
y is Element of the carrier of (a_net T)
the InternalRel of ((a_net T) * x) is Relation-like the carrier of ((a_net T) * x) -defined the carrier of ((a_net T) * x) -valued Element of bool [: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):]
[: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):] is non empty Relation-like set
bool [: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):] is non empty set
RelStr(# the carrier of ((a_net T) * x), the InternalRel of ((a_net T) * x) #) is strict RelStr
the InternalRel of (a_net T) is Relation-like the carrier of (a_net T) -defined the carrier of (a_net T) -valued Element of bool [: the carrier of (a_net T), the carrier of (a_net T):]
RelStr(# the carrier of (a_net T), the InternalRel of (a_net T) #) is strict RelStr
b is Element of the carrier of (a_net T)
k is Element of the carrier of (a_net T)
y is Element of the carrier of ((a_net T) * x)
F . y is Element of the carrier of (a_net T)
F is Element of the carrier of ((a_net T) * x)
F is Element of the carrier of ((a_net T) * x)
the InternalRel of ((a_net T) * x) is Relation-like the carrier of ((a_net T) * x) -defined the carrier of ((a_net T) * x) -valued Element of bool [: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):]
[: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):] is non empty Relation-like set
bool [: the carrier of ((a_net T) * x), the carrier of ((a_net T) * x):] is non empty set
RelStr(# the carrier of ((a_net T) * x), the InternalRel of ((a_net T) * x) #) is strict RelStr
the InternalRel of (a_net T) is Relation-like the carrier of (a_net T) -defined the carrier of (a_net T) -valued Element of bool [: the carrier of (a_net T), the carrier of (a_net T):]
RelStr(# the carrier of (a_net T), the InternalRel of (a_net T) #) is strict RelStr
F . F is Element of the carrier of (a_net T)
[G,j2] `2 is Element of T
x . F is set
(x . F) `2 is set
f0 is Element of the carrier of L
p is Element of T
[f0,p] is V38() Element of [: the carrier of L,T:]
{f0,p} is finite set
{f0} is non empty trivial finite 1 -element set
{{f0,p},{f0}} is finite V50() set
[f0,p] `1 is Element of the carrier of L
[f0,p] `2 is Element of T
(x . F) `1 is set
((a_net T) * x) . F is Element of the carrier of L
the mapping of ((a_net T) * x) . F is Element of the carrier of L
the mapping of (a_net T) is non empty Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like V41( the carrier of (a_net T), the carrier of L) Element of bool [: the carrier of (a_net T), the carrier of L:]
[: the carrier of (a_net T), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (a_net T), the carrier of L:] is non empty set
the mapping of (a_net T) * x is Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like Element of bool [: the carrier of (a_net T), the carrier of L:]
( the mapping of (a_net T) * x) . F is set
y is Element of the carrier of (a_net T)
(a_net T) . y is Element of the carrier of L
the mapping of (a_net T) . y is Element of the carrier of L
A is Element of the carrier of (BoolePoset ([#] L))
y "\/" A is Element of the carrier of (BoolePoset ([#] L))
y \/ A is set
j2 is Element of bool the carrier of L
"/\" (j2,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))
a_net T is non empty reflexive transitive strict directed V266(L) NetStr over L
(L,([#] L),T) is Element of the carrier of L
{ ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is Element of bool the carrier of L : b<sub>1</sub> in T } is set
"\/" ( { ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is Element of bool the carrier of L : b<sub>1</sub> in T } ,L) is Element of the carrier of L
x is non empty transitive directed subnet of a_net T
lim_inf x is Element of the carrier of L
lim_inf (a_net T) is Element of the carrier of L
the carrier of (a_net T) is non empty set
[: the carrier of (a_net T), the carrier of (a_net T):] is non empty Relation-like set
bool [: the carrier of (a_net T), the carrier of (a_net T):] is non empty set
y is Relation-like the carrier of (a_net T) -defined the carrier of (a_net T) -valued Function-like V41( the carrier of (a_net T), the carrier of (a_net T)) greater_or_equal_to_id Element of bool [: the carrier of (a_net T), the carrier of (a_net T):]
(a_net T) * y is non empty transitive strict directed subnet of a_net T
inf ((a_net T) * y) is Element of the carrier of L
L is non empty 1-sorted
the carrier of L is non empty set
T is non empty transitive directed NetStr over L
x is set
T " x is transitive strict V251(L,T) SubNetStr of T
y is non empty transitive strict directed subnet of T
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of L -valued Function-like V41( the carrier of y, the carrier of L) Element of bool [: the carrier of y, the carrier of L:]
the carrier of y is non empty set
[: the carrier of y, the carrier of L:] is non empty Relation-like set
bool [: the carrier of y, the carrier of L:] is non empty set
rng the mapping of y is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
z is set
dom the mapping of y is non empty Element of bool the carrier of y
bool the carrier of y is non empty set
x is set
the mapping of y . x is set
the carrier of T is non empty set
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
[: the carrier of T, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T, the carrier of L:] is non empty set
the mapping of T | the carrier of y is Relation-like the carrier of y -defined the carrier of T -defined the carrier of L -valued Function-like Element of bool [: the carrier of T, the carrier of L:]
dom ( the mapping of T | the carrier of y) is Element of bool the carrier of T
bool the carrier of T is non empty set
dom the mapping of T is non empty Element of bool the carrier of T
(dom the mapping of T) /\ the carrier of y is Element of bool the carrier of T
the mapping of T " x is Element of bool the carrier of T
( the mapping of T | the carrier of y) . x is set
the mapping of T . x is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
[#] L is non empty non proper open directed filtered lower upper Element of bool the carrier of L
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty Element of bool the carrier of L
xi L is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
lim_inf-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set
bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of L : for b<sub>2</sub> being Element of the carrier of L holds
( not b<sub>2</sub> in b<sub>1</sub> or for b<sub>3</sub> being non empty transitive directed NetStr over L holds
( not [b<sub>3</sub>,b<sub>2</sub>] in lim_inf-Convergence L or b<sub>3</sub> is_eventually_in b<sub>1</sub> ) ) } is set
T ` is Element of bool the carrier of L
the carrier of L \ T is set
the topology of L is Element of bool (bool the carrier of L)
y is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))
a_net y is non empty reflexive transitive strict directed V266(L) NetStr over L
(L,([#] L),y) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in y } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in y } ,L) is Element of the carrier of L
NetUniv L is non empty set
z is non empty transitive directed subnet of a_net y
lim_inf z is Element of the carrier of L
[(a_net y),(L,([#] L),y)] is V38() set
{(a_net y),(L,([#] L),y)} is finite set
{(a_net y)} is non empty trivial finite 1 -element set
{{(a_net y),(L,([#] L),y)},{(a_net y)}} is finite V50() set
z is Element of bool the carrier of L
the carrier of (a_net y) is non empty set
z is Element of the carrier of (a_net y)
{ [b₁,b₂] where b₁ is Element of the carrier of L, b₂ is Element of y : b₁ in b₂ } is set
x is Element of the carrier of L
y is Element of y
[x,y] is V38() Element of [: the carrier of L,y:]
[: the carrier of L,y:] is non empty Relation-like set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V50() set
A is Element of the carrier of (BoolePoset ([#] L))
F is Element of the carrier of (BoolePoset ([#] L))
a is Element of the carrier of (BoolePoset ([#] L))
the Element of a is Element of a
Bottom (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))
bool the carrier of L is non empty Element of bool (bool the carrier of L)
[ the Element of a,a] is V38() set
{ the Element of a,a} is finite set
{ the Element of a} is non empty trivial finite 1 -element set
{{ the Element of a,a},{ the Element of a}} is finite V50() set
G is Element of the carrier of (a_net y)
G `2 is set
z `2 is set
(a_net y) . G is Element of the carrier of L
the mapping of (a_net y) is non empty Relation-like the carrier of (a_net y) -defined the carrier of L -valued Function-like V41( the carrier of (a_net y), the carrier of L) Element of bool [: the carrier of (a_net y), the carrier of L:]
[: the carrier of (a_net y), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (a_net y), the carrier of L:] is non empty set
the mapping of (a_net y) . G is Element of the carrier of L
G `1 is set
y is Element of the carrier of L
(T `) ` is Element of bool the carrier of L
the carrier of L \ (T `) is set
x is non empty transitive directed NetStr over L
[x,y] is V38() set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V50() set
y is non empty transitive strict directed subnet of x
the mapping of y is non empty Relation-like the carrier of y -defined the carrier of L -valued Function-like V41( the carrier of y, the carrier of L) Element of bool [: the carrier of y, the carrier of L:]
the carrier of y is non empty set
[: the carrier of y, the carrier of L:] is non empty Relation-like set
bool [: the carrier of y, the carrier of L:] is non empty set
rng the mapping of y is non empty Element of bool the carrier of L
[:(NetUniv L), the carrier of L:] is non empty Relation-like set
the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski universal set
the Element of the carrier of y is Element of the carrier of y
y | the Element of the carrier of y is non empty transitive strict directed subnet of y
the mapping of (y | the Element of the carrier of y) is non empty Relation-like the carrier of (y | the Element of the carrier of y) -defined the carrier of L -valued Function-like V41( the carrier of (y | the Element of the carrier of y), the carrier of L) Element of bool [: the carrier of (y | the Element of the carrier of y), the carrier of L:]
the carrier of (y | the Element of the carrier of y) is non empty set
[: the carrier of (y | the Element of the carrier of y), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | the Element of the carrier of y), the carrier of L:] is non empty set
rng the mapping of (y | the Element of the carrier of y) is non empty Element of bool the carrier of L
{ (rng the mapping of (y | b₁)) where b₁ is Element of the carrier of y : verum } is set
G is set
bool ([#] L) is non empty Element of bool (bool ([#] L))
bool ([#] L) is non empty set
bool (bool ([#] L)) is non empty set
F is Element of the carrier of y
y | F is non empty transitive strict directed subnet of y
the mapping of (y | F) is non empty Relation-like the carrier of (y | F) -defined the carrier of L -valued Function-like V41( the carrier of (y | F), the carrier of L) Element of bool [: the carrier of (y | F), the carrier of L:]
the carrier of (y | F) is non empty set
[: the carrier of (y | F), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | F), the carrier of L:] is non empty set
rng the mapping of (y | F) is non empty Element of bool the carrier of L
G is non empty Element of bool the carrier of (BoolePoset ([#] L))
fininfs G is non empty filtered Element of bool the carrier of (BoolePoset ([#] L))
bool G is non empty set
{ ("/\" (b₁,(BoolePoset ([#] L)))) where b₁ is finite Element of bool G : ex_inf_of b₁, BoolePoset ([#] L) } is set
F is set
F is Element of the carrier of (BoolePoset ([#] L))
the mapping of y | the carrier of (y | the Element of the carrier of y) is Relation-like the carrier of y -defined the carrier of (y | the Element of the carrier of y) -defined the carrier of y -defined the carrier of L -valued Function-like Element of bool [: the carrier of y, the carrier of L:]
rng ( the mapping of y | the carrier of (y | the Element of the carrier of y)) is Element of bool the carrier of L
dom ( the mapping of y | the carrier of (y | the Element of the carrier of y)) is Element of bool the carrier of y
bool the carrier of y is non empty set
y is set
( the mapping of y | the carrier of (y | the Element of the carrier of y)) . y is set
dom the mapping of y is non empty Element of bool the carrier of y
(dom the mapping of y) /\ the carrier of (y | the Element of the carrier of y) is Element of bool the carrier of y
the mapping of y . y is set
a is Element of the carrier of (BoolePoset ([#] L))
uparrow (fininfs G) is non empty filtered upper Element of bool the carrier of (BoolePoset ([#] L))
z is Element of the carrier of L
lim_inf y is Element of the carrier of L
{ (inf (y | b₁)) where b₁ is Element of the carrier of y : verum } is set
"\/" ( { (inf (y | b₁)) where b₁ is Element of the carrier of y : verum } ,L) is Element of the carrier of L
the carrier of x is non empty set
F is non empty transitive strict directed NetStr over L
the carrier of F is non empty set
F is finite Element of bool G
"/\" (F,(BoolePoset ([#] L))) is Element of the carrier of (BoolePoset ([#] L))
"/\" ({},(BoolePoset ([#] L))) is Element of the carrier of (BoolePoset ([#] L))
Top (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))
y is finite Element of bool the carrier of (BoolePoset ([#] L))
f0 is set
p is Element of the carrier of y
y | p is non empty transitive strict directed subnet of y
the mapping of (y | p) is non empty Relation-like the carrier of (y | p) -defined the carrier of L -valued Function-like V41( the carrier of (y | p), the carrier of L) Element of bool [: the carrier of (y | p), the carrier of L:]
the carrier of (y | p) is non empty set
[: the carrier of (y | p), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | p), the carrier of L:] is non empty set
rng the mapping of (y | p) is non empty Element of bool the carrier of L
f0 is Relation-like Function-like set
proj1 f0 is set
proj2 f0 is set
[#] y is non empty non proper lower upper Element of bool the carrier of y
bool ([#] y) is non empty set
p is finite Element of bool ([#] y)
b is Element of the carrier of y
y | b is non empty transitive strict directed subnet of y
the mapping of (y | b) is non empty Relation-like the carrier of (y | b) -defined the carrier of L -valued Function-like V41( the carrier of (y | b), the carrier of L) Element of bool [: the carrier of (y | b), the carrier of L:]
the carrier of (y | b) is non empty set
[: the carrier of (y | b), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | b), the carrier of L:] is non empty set
rng the mapping of (y | b) is non empty Element of bool the carrier of L
k is set
f0 . k is set
l is Element of the carrier of y
y | l is non empty transitive strict directed subnet of y
the mapping of (y | l) is non empty Relation-like the carrier of (y | l) -defined the carrier of L -valued Function-like V41( the carrier of (y | l), the carrier of L) Element of bool [: the carrier of (y | l), the carrier of L:]
the carrier of (y | l) is non empty set
[: the carrier of (y | l), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | l), the carrier of L:] is non empty set
rng the mapping of (y | l) is non empty Element of bool the carrier of L
pj9 is Element of the carrier of y
pj is set
the mapping of y | the carrier of (y | b) is Relation-like the carrier of y -defined the carrier of (y | b) -defined the carrier of y -defined the carrier of L -valued Function-like Element of bool [: the carrier of y, the carrier of L:]
rng ( the mapping of y | the carrier of (y | b)) is Element of bool the carrier of L
dom ( the mapping of y | the carrier of (y | b)) is Element of bool the carrier of y
q is set
( the mapping of y | the carrier of (y | b)) . q is set
(dom the mapping of y) /\ the carrier of (y | b) is Element of bool the carrier of y
{ b₁ where b₁ is Element of the carrier of y : b <= b₁ } is set
n9 is Element of the carrier of y
{ b₁ where b₁ is Element of the carrier of y : l <= b₁ } is set
(dom the mapping of y) /\ the carrier of (y | l) is Element of bool the carrier of y
the mapping of y | the carrier of (y | l) is Relation-like the carrier of y -defined the carrier of (y | l) -defined the carrier of y -defined the carrier of L -valued Function-like Element of bool [: the carrier of y, the carrier of L:]
dom ( the mapping of y | the carrier of (y | l)) is Element of bool the carrier of y
the mapping of y . q is set
( the mapping of y | the carrier of (y | l)) . q is set
rng ( the mapping of y | the carrier of (y | l)) is Element of bool the carrier of L
meet y is set
F is Element of the carrier of (BoolePoset ([#] L))
F is non empty filtered upper Element of bool the carrier of (BoolePoset ([#] L))
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in F } is set
y is set
f0 is Element of the carrier of y
y | f0 is non empty transitive strict directed subnet of y
inf (y | f0) is Element of the carrier of L
the mapping of (y | f0) is non empty Relation-like the carrier of (y | f0) -defined the carrier of L -valued Function-like V41( the carrier of (y | f0), the carrier of L) Element of bool [: the carrier of (y | f0), the carrier of L:]
the carrier of (y | f0) is non empty set
[: the carrier of (y | f0), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | f0), the carrier of L:] is non empty set
rng the mapping of (y | f0) is non empty Element of bool the carrier of L
p is Element of bool the carrier of L
//\ ( the mapping of (y | f0),L) is Element of the carrier of L
"/\" ((rng the mapping of (y | f0)),L) is Element of the carrier of L
y is non empty transitive directed subnet of y
lim_inf y is Element of the carrier of L
y is non empty transitive directed subnet of y
lim_inf y is Element of the carrier of L
y is Element of the carrier of L
f0 is Element of bool the carrier of L
"/\" (f0,L) is Element of the carrier of L
p is Element of the carrier of y
y | p is non empty transitive strict directed subnet of y
the mapping of (y | p) is non empty Relation-like the carrier of (y | p) -defined the carrier of L -valued Function-like V41( the carrier of (y | p), the carrier of L) Element of bool [: the carrier of (y | p), the carrier of L:]
the carrier of (y | p) is non empty set
[: the carrier of (y | p), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y | p), the carrier of L:] is non empty set
rng the mapping of (y | p) is non empty Element of bool the carrier of L
f0 /\ (rng the mapping of (y | p)) is Element of bool the carrier of L
b is Element of the carrier of L
dom the mapping of (y | p) is non empty Element of bool the carrier of (y | p)
bool the carrier of (y | p) is non empty set
k is set
the mapping of (y | p) . k is set
{ b₁ where b₁ is Element of the carrier of y : p <= b₁ } is set
l is Element of the carrier of y
pj is Element of the carrier of y
y . pj is Element of the carrier of L
the mapping of y . pj is Element of the carrier of L
pj9 is Element of the carrier of (y | p)
(y | p) . pj9 is Element of the carrier of L
the mapping of (y | p) . pj9 is Element of the carrier of L
the mapping of (y | p) . pj9 is Element of the carrier of L
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
p is Relation-like the carrier of y -defined the carrier of y -valued Function-like V41( the carrier of y, the carrier of y) Element of bool [: the carrier of y, the carrier of y:]
y * p is non empty transitive strict directed NetStr over L
the mapping of (y * p) is non empty Relation-like the carrier of (y * p) -defined the carrier of L -valued Function-like V41( the carrier of (y * p), the carrier of L) Element of bool [: the carrier of (y * p), the carrier of L:]
the carrier of (y * p) is non empty set
[: the carrier of (y * p), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (y * p), the carrier of L:] is non empty set
rng the mapping of (y * p) is non empty Element of bool the carrier of L
b is set
{ ((y * p) . b₁) where b₁ is Element of the carrier of (y * p) : verum } is set
k is Element of the carrier of (y * p)
(y * p) . k is Element of the carrier of L
the mapping of (y * p) . k is Element of the carrier of L
dom p is Element of bool the carrier of y
the mapping of y * p is Relation-like the carrier of y -defined the carrier of L -valued Function-like Element of bool [: the carrier of y, the carrier of L:]
( the mapping of y * p) . k is set
l is Element of the carrier of y
p . l is Element of the carrier of y
y . (p . l) is Element of the carrier of L
the mapping of y . (p . l) is Element of the carrier of L
"/\" ((rng the mapping of (y * p)),L) is Element of the carrier of L
b is non empty transitive directed subnet of y
inf b is Element of the carrier of L
inf (y * p) is Element of the carrier of L
//\ ( the mapping of (y * p),L) is Element of the carrier of L
(L,([#] L),F) is Element of the carrier of L
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in F } ,L) is Element of the carrier of L
L is non empty reflexive RelStr
sigma L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
xi L is Element of bool (bool the carrier of L)
T is set
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T is non empty TopSpace-like TopStruct
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of L is Element of bool (bool the carrier of L)
x is quasi_prebasis V269(L) Element of bool (bool the carrier of L)
y is set
FinMeetCl x is Element of bool (bool the carrier of L)
UniCl (FinMeetCl x) is Element of bool (bool the carrier of L)
z is Element of bool (bool the carrier of L)
union z is Element of bool the carrier of L
x is set
y is Element of bool (bool the carrier of L)
Intersect y is Element of bool the carrier of L
A is Element of bool (bool the carrier of T)
meet A is Element of bool the carrier of T
Intersect A is Element of bool the carrier of T
FinMeetCl the topology of T is Element of bool (bool the carrier of T)
x is Element of bool (bool the carrier of T)
union x is Element of bool the carrier of T
UniCl the topology of T is Element of bool (bool the carrier of T)
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
omega L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
xi L is Element of bool (bool the carrier of L)
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L) is non empty set
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L : verum } is set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L #) is strict RelStr
y is quasi_prebasis V269( the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L) Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L)
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L) is non empty set
z is set
x is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
uparrow x is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
uparrow {x} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
(uparrow x) ` is lower Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L \ (uparrow x) is set
y is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
uparrow y is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
{y} is non empty trivial finite 1 -element Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
uparrow {y} is non empty upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
"/\" ((uparrow y), the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
[#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty non proper open directed filtered lower upper Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
BoolePoset ([#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)) is non empty set
F is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L))
{ ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L : b₁ in F } is set
"\/" ( { ("/\" (b₁, the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)) where b₁ is Element of bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L : b₁ in F } , the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
( the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L,([#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L),F) is Element of the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L)
L is TopSpace-like TopStruct
T is TopSpace-like TopStruct
x is non empty TopSpace-like TopStruct
the carrier of L is set
the carrier of x is non empty set
the topology of L is Element of bool (bool the carrier of L)
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of x is Element of bool (bool the carrier of x)
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
the carrier of T is set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
y is TopSpace-like Refinement of L,T
the carrier of y is set
the carrier of x \/ the carrier of x is set
the topology of y is Element of bool (bool the carrier of y)
bool the carrier of y is non empty set
bool (bool the carrier of y) is non empty set
the topology of L \/ the topology of T is set
z is quasi_prebasis V269(y) Element of bool (bool the carrier of y)
FinMeetCl z is Element of bool (bool the carrier of y)
UniCl (FinMeetCl z) is Element of bool (bool the carrier of y)
FinMeetCl the topology of x is Element of bool (bool the carrier of x)
UniCl (FinMeetCl the topology of x) is Element of bool (bool the carrier of x)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
T is TopSpace-like TopExtension of L
the carrier of T is set
bool the carrier of T is non empty set
x is Element of bool the carrier of L
[#] T is non proper open Element of bool the carrier of T
y is Element of bool the carrier of T
([#] T) \ y is Element of bool the carrier of T
the topology of L is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
[#] L is non proper open Element of bool the carrier of L
([#] L) \ x is Element of bool the carrier of L
z is Element of bool the carrier of T
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
lambda L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
xi L is Element of bool (bool the carrier of L)
the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L)
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L) is non empty set
omega L is Element of bool (bool the carrier of L)
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L) is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of L #) is strict RelStr
sigma L is Element of bool (bool the carrier of L)
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L)
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L is non empty set
bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L) is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of L #) is strict RelStr
the topology of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is Element of bool (bool the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L)
the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty set
bool the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty set
bool (bool the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopAugmentation of L
x is non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L
lambda L is Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of x is Element of bool (bool the carrier of x)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
xi L is Element of bool (bool the carrier of L)
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopRelStr
[#] L is non empty non proper open directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
T is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))
(L,([#] L),T) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in T } ,L) is Element of the carrier of L
y is Element of bool the carrier of L
([#] L) \ y is Element of bool the carrier of L
y ` is Element of bool the carrier of L
the carrier of L \ y is set
L is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L
[#] L is non empty non proper open directed filtered lower upper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is non empty set
BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr
the carrier of (BoolePoset ([#] L)) is non empty non trivial set
bool the carrier of (BoolePoset ([#] L)) is non empty set
x is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))
(L,([#] L),x) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in x } is set
"\/" ( { ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in x } ,L) is Element of the carrier of L
y is Element of the carrier of L
z is Element of the carrier of L
x is Element of the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty set
the InternalRel of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is Relation-like the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L -defined the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L -valued Element of bool [: the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L, the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L:]
[: the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L, the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L, the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L, the InternalRel of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L #) is strict RelStr
y is Element of the carrier of L
z is Element of the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L
{z} is non empty trivial finite 1 -element closed Element of bool the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L
bool the carrier of the non empty TopSpace-like T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of L is non empty set
{y} is non empty trivial finite 1 -element Element of bool the carrier of L
{x} is non empty trivial finite 1 -element Element of bool the carrier of L
Cl {x} is closed Element of bool the carrier of L