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)
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 in x } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 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
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 in z } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 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
{ ("/\" (b1,T)) where b1 is Element of bool the carrier of T : b1 in x } is set
"\/" ( { ("/\" (b1,T)) where b1 is Element of bool the carrier of T : b1 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 . b1) where b1 is Element of the carrier of y : a1 <= b1 } is set
{ (x . b1) where b1 is Element of the carrier of x : a1 <= b1 } is set
z is Element of the carrier of x
x is Element of the carrier of y
{ (x . b1) where b1 is Element of the carrier of x : z <= b1 } is set
{ (y . b1) where b1 is Element of the carrier of y : x <= b1 } 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 . b1) where b1 is Element of the carrier of y : a1 <= b1 } is set
{ (x . b1) where b1 is Element of the carrier of x : a1 <= b1 } is set
{ ("/\" (H2(b1),L)) where b1 is Element of the carrier of x : verum } is set
{ ("/\" (H1(b1),T)) where b1 is Element of the carrier of y : verum } is set
y is set
A is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : A <= b1 } is set
"/\" (H2(A),L) is Element of the carrier of L
F is Element of the carrier of y
{ (y . b1) where b1 is Element of the carrier of y : F <= b1 } is set
a is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : a <= b1 } 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
"/\" (H1(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 . b1) where b1 is Element of the carrier of y : a1 <= b1 } is set
{ (x . b1) where b1 is Element of the carrier of x : a1 <= b1 } is set
{ ("/\" (H2(b1),L)) where b1 is Element of the carrier of x : verum } is set
{ ("/\" (H1(b1),T)) where b1 is Element of the carrier of y : verum } is set
"\/" ( { ("/\" (H2(b1),L)) where b1 is Element of the carrier of x : verum } ,L) is Element of the carrier of L
"\/" ( { ("/\" (H1(b1),T)) where b1 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 . b1) where b1 is Element of the carrier of x : A <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : A <= b1 } ,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
{ b1 where b1 is Element of bool the carrier of T : for b2 being Element of the carrier of T holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over T holds
( not [b3,b2] in lim_inf-Convergence T or b3 is_eventually_in b1 ) ) } is set
bool the carrier of L is non empty set
{ b1 where b1 is Element of bool the carrier of L : for b2 being Element of the carrier of L holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over L holds
( not [b3,b2] in lim_inf-Convergence L or b3 is_eventually_in b1 ) ) } 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 | b1)) where b1 is Element of the carrier of T : verum } is set
"\/" ( { (inf (T | b1)) where b1 is Element of the carrier of T : verum } ,L) is Element of the carrier of L
{ ("/\" ( { (T . b2) where b2 is Element of the carrier of T : b1 <= b2 } ,L)) where b1 is Element of the carrier of T : verum } is set
z is set
x is Element of the carrier of T
{ (T . b1) where b1 is Element of the carrier of T : x <= b1 } is set
"/\" ( { (T . b1) where b1 is Element of the carrier of T : x <= b1 } ,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) . b1) where b1 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
{ b1 where b1 is Element of the carrier of T : F <= b1 } 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
{ b1 where b1 is Element of the carrier of T : F <= b1 } 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) . b1) where b1 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 . b2) where b2 is Element of the carrier of T : b1 <= b2 } ,L)) where b1 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 . b1) where b1 is Element of the carrier of T : x <= b1 } 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) . b1) where b1 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
{ b1 where b1 is Element of the carrier of T : x <= b1 } 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
{ b1 where b1 is Element of the carrier of T : x <= b1 } 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) . b1) where b1 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
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } 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)
{ b1 where b1 is Element of the carrier of (a_net T) : y <= b1 } 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) . b1) where b1 is Element of the carrier of ((a_net T) | y) : verum } is set
z is set
{ (((a_net T) | y) . b1) where b1 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
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } is set
{ b1 where b1 is Element of the carrier of (a_net T) : y <= b1 } 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
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 in T } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 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) | b1)) where b1 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)
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } 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
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } 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) | b1)) where b1 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))
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } 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
{ [b1,b2] where b1 is Element of the carrier of L, b2 is Element of T : b1 in b2 } 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
{ ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 in T } is set
"\/" ( { ("/\" (b1,L)) where b1 is Element of bool the carrier of L : b1 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