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

1 is non empty set

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

the carrier of () is non empty non trivial set
bool the carrier of () is non empty set
x is non empty filtered upper Element of bool the carrier of ()
{ ("/\" (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

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

the carrier of () is non empty non trivial set
bool the carrier of () is non empty set
y is non empty Element of bool the carrier of T

the carrier of () is non empty non trivial set
bool the carrier of () is non empty set
z is non empty filtered upper Element of bool the carrier of ()
(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 ()
(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

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 is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) 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 )
union y is Element of bool the carrier of
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

the carrier of L is non empty set

the carrier of is non empty set

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

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)

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

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

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

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

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 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 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
[:(), 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

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

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 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 topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) is non empty set

the topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) 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

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 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 topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) is non empty set
the topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) is non empty set

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

the topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) is non empty set

the topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is non empty set
bool (bool the carrier of ) is non empty set

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

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

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

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)

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

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

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

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)

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

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 () 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 ()
y `2 is set
() | y is non empty reflexive transitive strict directed subnet of a_net T
inf (() | y) is Element of the carrier of L
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
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 ()
[x,y] `1 is Element of the carrier of L
() . A is Element of the carrier of L
the mapping of () is non empty Relation-like the carrier of () -defined the carrier of L -valued Function-like V41( the carrier of (), the carrier of L) Element of bool [: the carrier of (), the carrier of L:]
[: the carrier of (), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (), the carrier of L:] is non empty set
the mapping of () . 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 ()
{ b1 where b1 is Element of the carrier of () : y <= b1 } is set
a is Element of the carrier of (() | y)
() . F is Element of the carrier of L
the mapping of () . F is Element of the carrier of L
j2 is Element of the carrier of (() | y)
(() | y) . j2 is Element of the carrier of L
the mapping of (() | y) . j2 is Element of the carrier of L
{ ((() | y) . b1) where b1 is Element of the carrier of (() | y) : verum } is set
z is set
{ ((() | y) . b1) where b1 is Element of the carrier of (() | y) : verum } is set
x is Element of the carrier of (() | y)
(() | y) . x is Element of the carrier of L
the mapping of (() | 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 () : y <= b1 } is set
y is Element of the carrier of ()
y `2 is set
A is Element of the carrier of ()
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
() . y is Element of the carrier of L
the mapping of () is non empty Relation-like the carrier of () -defined the carrier of L -valued Function-like V41( the carrier of (), the carrier of L) Element of bool [: the carrier of (), the carrier of L:]
[: the carrier of (), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (), the carrier of L:] is non empty set
the mapping of () . y is Element of the carrier of L
a is Element of the carrier of (() | y)
(() | y) . a is Element of the carrier of L
the mapping of (() | y) . a is Element of the carrier of L
y `1 is set
//\ ( the mapping of (() | y),L) is Element of the carrier of L
"/\" ((rng the mapping of (() | y)),L) is Element of the carrier of L

[#] 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

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 () is Element of the carrier of L
the carrier of () is non empty set
{ (inf (() | b1)) where b1 is Element of the carrier of () : verum } is set
z is set
x is Element of the carrier of ()
() | x is non empty reflexive transitive strict directed subnet of a_net T
inf (() | x) is Element of the carrier of L
y is Element of the carrier of ()
{ [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 is non empty reflexive transitive strict directed subnet of a_net T
inf (() | 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 ()
() | F is non empty reflexive transitive strict directed subnet of a_net T
inf (() | F) is Element of the carrier of L
"\/" ( { (inf (() | b1)) where b1 is Element of the carrier of () : verum } ,L) is Element of the carrier of L

[#] 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

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

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

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 () is non empty set

[#] 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

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 () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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 () -defined the carrier of () -valued Function-like V41( the carrier of (), the carrier of ()) greater_or_equal_to_id Element of bool [: the carrier of (), the carrier of ():]
() * x is non empty transitive strict directed subnet of a_net T
inf (() * x) is Element of the carrier of L
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) is non empty set
[: 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
rng the mapping of (() * x) is non empty Element of bool the carrier of L
the Element of T is Element of T
//\ ( the mapping of (() * x),L) is Element of the carrier of L
"/\" ((rng the mapping of (() * 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 (() * 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 (() * x)) is Element of bool the carrier of L
[: the carrier of (() * x), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (() * x), the carrier of ():] 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