:: WAYBEL28 semantic presentation

K37() is set
bool K37() is set
K165() is set
bool K165() is set
K169() is Element of bool K165()
{} is set

1 is non empty set

A is non empty transitive directed NetStr over L
inf A is Element of the carrier of L
the carrier of L is non empty set
lim_inf A is Element of the carrier of L
the carrier of A is non empty set
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
A1 is set
A9 is Element of the carrier of A
{ (A . b1) where b1 is Element of the carrier of A : A9 <= b1 } is set
"/\" ( { (A . b1) where b1 is Element of the carrier of A : A9 <= b1 } ,L) is Element of the carrier of L
bool the carrier of L is set
the Element of the carrier of A is Element of the carrier of A
{ (A . b1) where b1 is Element of the carrier of A : the Element of the carrier of A <= b1 } is set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
rng the mapping of A is non empty Element of bool the carrier of L
A9 is set
dom the mapping of A is non empty Element of bool the carrier of A
bool the carrier of A is set
x1 is Element of the carrier of A
A . x1 is Element of the carrier of L
the mapping of A . x1 is Element of the carrier of L
A1 is Element of bool the carrier of L
"/\" ( { (A . b1) where b1 is Element of the carrier of A : the Element of the carrier of A <= b1 } ,L) is Element of the carrier of L
"/\" ((rng the mapping of A),L) is Element of the carrier of L
//\ ( the mapping of A,L) is Element of the carrier of L
A9 is Element of bool the carrier of L
"\/" (A9,L) is Element of the carrier of L

the carrier of L is non empty set
A is non empty transitive directed NetStr over L
lim_inf A is Element of the carrier of L
the carrier of A is non empty set
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
T is Element of the carrier of L
A1 is non empty transitive directed subnet of A
inf A1 is Element of the carrier of L
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L

the carrier of L is non empty set
NetUniv L is non empty set
A is non empty transitive directed NetStr over L
lim_inf A is Element of the carrier of L
the carrier of A is non empty set
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
T is Element of the carrier of L
A1 is non empty transitive directed subnet of A
inf A1 is Element of the carrier of L
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is set
L is non empty reflexive RelStr
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V34( the carrier of L) V35( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is set
id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V34( the carrier of L) V35( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
A is Element of the carrier of L
(id L) . A is Element of the carrier of L
T is Element of the carrier of L
(id L) . T is Element of the carrier of L
L is non empty directed RelStr
the carrier of L is non empty set
A is Element of the carrier of L
T is Element of the carrier of L
[#] L is non empty non proper lower upper Element of bool the carrier of L
bool the carrier of L is set
A1 is Element of the carrier of L
L is non empty directed RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is set
A is set
T is Element of the carrier of L
A1 is Element of the carrier of L
A9 is Element of the carrier of L
A9 is Element of the carrier of L

dom A is set
rng A is set
T is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V34( the carrier of L) V35( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
A1 is Element of the carrier of L
T . A1 is Element of the carrier of L
L is non empty reflexive RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is set
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V34( the carrier of L) V35( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V34( the carrier of L) V35( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty 1-sorted
A is non empty NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is 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:]
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
the carrier of L is non empty set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
the mapping of A * T is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is non empty strict NetStr over L
the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is non empty set
the InternalRel of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is Relation-like the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) -defined the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) -valued Element of bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #):]
[: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #):] is Relation-like set
bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #):] is set
RelStr(# the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the InternalRel of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) #) is strict RelStr
the mapping of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is non empty Relation-like the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) -defined the carrier of L -valued Function-like V34( the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #)) V35( the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of L) Element of bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of L:]
[: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of L:] is Relation-like set
bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #), the carrier of L:] is set
A1 is non empty strict NetStr over L
the carrier of A1 is non empty set
the InternalRel of A1 is Relation-like the carrier of A1 -defined the carrier of A1 -valued Element of bool [: the carrier of A1, the carrier of A1:]
[: the carrier of A1, the carrier of A1:] is Relation-like set
bool [: the carrier of A1, the carrier of A1:] is set
RelStr(# the carrier of A1, the InternalRel of A1 #) is strict RelStr
the mapping of A1 is non empty Relation-like the carrier of A1 -defined the carrier of L -valued Function-like V34( the carrier of A1) V35( the carrier of A1, the carrier of L) Element of bool [: the carrier of A1, the carrier of L:]
[: the carrier of A1, the carrier of L:] is Relation-like set
bool [: the carrier of A1, the carrier of L:] is set
A9 is non empty strict NetStr over L
the carrier of A9 is non empty set
the InternalRel of A9 is Relation-like the carrier of A9 -defined the carrier of A9 -valued Element of bool [: the carrier of A9, the carrier of A9:]
[: the carrier of A9, the carrier of A9:] is Relation-like set
bool [: the carrier of A9, the carrier of A9:] is set
RelStr(# the carrier of A9, the InternalRel of A9 #) is strict RelStr
the mapping of A9 is non empty Relation-like the carrier of A9 -defined the carrier of L -valued Function-like V34( the carrier of A9) V35( the carrier of A9, the carrier of L) Element of bool [: the carrier of A9, the carrier of L:]
[: the carrier of A9, the carrier of L:] is Relation-like set
bool [: the carrier of A9, the carrier of L:] is set
L is non empty 1-sorted
A is non empty NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty strict NetStr over L
the carrier of (L,A,T) is non empty set
the InternalRel of (L,A,T) is Relation-like the carrier of (L,A,T) -defined the carrier of (L,A,T) -valued Element of bool [: the carrier of (L,A,T), the carrier of (L,A,T):]
[: the carrier of (L,A,T), the carrier of (L,A,T):] is Relation-like set
bool [: the carrier of (L,A,T), the carrier of (L,A,T):] is set
RelStr(# the carrier of (L,A,T), the InternalRel of (L,A,T) #) is strict RelStr
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:]
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
L is non empty 1-sorted
the carrier of L is non empty set
A is non empty NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is 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 mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty strict NetStr over L
the mapping of A * T is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is non empty strict NetStr over L
the carrier of (L,A,T) is non empty set
the InternalRel of (L,A,T) is Relation-like the carrier of (L,A,T) -defined the carrier of (L,A,T) -valued Element of bool [: the carrier of (L,A,T), the carrier of (L,A,T):]
[: the carrier of (L,A,T), the carrier of (L,A,T):] is Relation-like set
bool [: the carrier of (L,A,T), the carrier of (L,A,T):] is set
RelStr(# the carrier of (L,A,T), the InternalRel of (L,A,T) #) is strict RelStr
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
L is non empty 1-sorted
the carrier of L is non empty set
A is non empty transitive directed RelStr
the carrier of A is non empty set
[: the carrier of A, the carrier of L:] is Relation-like set
bool [: the carrier of A, the carrier of L:] is 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 Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
NetStr(# the carrier of A, the InternalRel of A,T #) is non empty strict NetStr over L
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
the carrier of NetStr(# the carrier of A, the InternalRel of A,T #) is non empty set
the InternalRel of NetStr(# the carrier of A, the InternalRel of A,T #) is Relation-like the carrier of NetStr(# the carrier of A, the InternalRel of A,T #) -defined the carrier of NetStr(# the carrier of A, the InternalRel of A,T #) -valued Element of bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,T #), the carrier of NetStr(# the carrier of A, the InternalRel of A,T #):]
[: the carrier of NetStr(# the carrier of A, the InternalRel of A,T #), the carrier of NetStr(# the carrier of A, the InternalRel of A,T #):] is Relation-like set
bool [: the carrier of NetStr(# the carrier of A, the InternalRel of A,T #), the carrier of NetStr(# the carrier of A, the InternalRel of A,T #):] is set
RelStr(# the carrier of NetStr(# the carrier of A, the InternalRel of A,T #), the InternalRel of NetStr(# the carrier of A, the InternalRel of A,T #) #) is strict RelStr
[#] A is non empty non proper lower upper Element of bool the carrier of A
bool the carrier of A is set
[#] NetStr(# the carrier of A, the InternalRel of A,T #) is non empty non proper lower upper Element of bool the carrier of NetStr(# the carrier of A, the InternalRel of A,T #)
bool the carrier of NetStr(# the carrier of A, the InternalRel of A,T #) is set
A is non empty transitive directed RelStr
the carrier of A is non empty set
L is non empty 1-sorted
the carrier of L is non empty set
[: the carrier of A, the carrier of L:] is Relation-like set
bool [: the carrier of A, the carrier of L:] is 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 Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
NetStr(# the carrier of A, the InternalRel of A,T #) is non empty strict NetStr over L
L is non empty 1-sorted
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty strict NetStr over L
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 L is non empty set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
the mapping of A * T is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
NetStr(# the carrier of A, the InternalRel of A,( the mapping of A * T) #) is non empty transitive strict directed NetStr over L
L is non empty 1-sorted
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty strict NetStr over L
L is non empty 1-sorted
NetUniv L is non empty set
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty transitive strict directed NetStr over L
the carrier of L is non empty set

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
the carrier of (L,A,T) is non empty set
A1 is non empty transitive strict directed NetStr over L
the carrier of A1 is non empty set
L is non empty 1-sorted
A is non empty transitive directed NetStr over L
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 Relation-like set
bool [: the carrier of A, the carrier of A:] is set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
the carrier of L is non empty set
[: the carrier of A, the carrier of L:] is Relation-like set
bool [: the carrier of A, the carrier of L:] is set
NetStr(# the carrier of A, the InternalRel of A, the mapping of A #) is non empty transitive strict directed NetStr over L
T is non empty transitive directed NetStr over L
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 Relation-like set
bool [: the carrier of T, the carrier of T:] is set
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( 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 Relation-like set
bool [: the carrier of T, the carrier of L:] is set
NetStr(# the carrier of T, the InternalRel of T, the mapping of T #) is non empty transitive strict directed NetStr over L
[: the carrier of T, the carrier of A:] is Relation-like set
bool [: the carrier of T, the carrier of A:] is set
A1 is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
the mapping of A * A1 is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
A9 is non empty Relation-like the carrier of T -defined the carrier of A -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of A) Element of bool [: the carrier of T, the carrier of A:]
the mapping of A * A9 is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
A9 is Element of the carrier of A
x1 is Element of the carrier of A
x is Element of the carrier of T
x is Element of the carrier of T
A9 . x is Element of the carrier of A
[x,x] is set
{x,x} is set
{x} is set
{{x,x},{x}} is set
p is Element of the carrier of A
A1 is non empty Relation-like the carrier of T -defined the carrier of A -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of A) Element of bool [: the carrier of T, the carrier of A:]
the mapping of A * A1 is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
L is non empty 1-sorted
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty transitive strict directed NetStr over L
the carrier of (L,A,T) is non empty set
[: the carrier of (L,A,T), the carrier of A:] is Relation-like set
bool [: the carrier of (L,A,T), the carrier of A:] is set
the carrier of L is non empty set
the mapping of (L,A,T) is non empty Relation-like the carrier of (L,A,T) -defined the carrier of L -valued Function-like V34( the carrier of (L,A,T)) V35( the carrier of (L,A,T), the carrier of L) Element of bool [: the carrier of (L,A,T), the carrier of L:]
[: the carrier of (L,A,T), the carrier of L:] is Relation-like set
bool [: the carrier of (L,A,T), the carrier of L:] is set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
A1 is non empty Relation-like the carrier of (L,A,T) -defined the carrier of A -valued Function-like V34( the carrier of (L,A,T)) V35( the carrier of (L,A,T), the carrier of A) Element of bool [: the carrier of (L,A,T), the carrier of A:]
the mapping of A * A1 is non empty Relation-like the carrier of (L,A,T) -defined the carrier of L -valued Function-like V34( the carrier of (L,A,T)) V35( the carrier of (L,A,T), the carrier of L) Element of bool [: the carrier of (L,A,T), the carrier of L:]
A9 is Element of the carrier of A
A9 is Element of the carrier of (L,A,T)
x1 is Element of the carrier of (L,A,T)
A1 . x1 is Element of the carrier of A
x is Element of the carrier of A
T . x is Element of the carrier of A
the InternalRel of (L,A,T) is Relation-like the carrier of (L,A,T) -defined the carrier of (L,A,T) -valued Element of bool [: the carrier of (L,A,T), the carrier of (L,A,T):]
[: the carrier of (L,A,T), the carrier of (L,A,T):] is Relation-like set
bool [: the carrier of (L,A,T), the carrier of (L,A,T):] is set
RelStr(# the carrier of (L,A,T), the InternalRel of (L,A,T) #) is strict RelStr
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:]
RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr
A1 is non empty Relation-like the carrier of (L,A,T) -defined the carrier of A -valued Function-like V34( the carrier of (L,A,T)) V35( the carrier of (L,A,T), the carrier of A) Element of bool [: the carrier of (L,A,T), the carrier of A:]
the mapping of A * A1 is non empty Relation-like the carrier of (L,A,T) -defined the carrier of L -valued Function-like V34( the carrier of (L,A,T)) V35( the carrier of (L,A,T), the carrier of L) Element of bool [: the carrier of (L,A,T), the carrier of L:]
L is non empty 1-sorted
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,T) is non empty transitive strict directed NetStr over L

the carrier of L is non empty set
A is non empty transitive directed NetStr over L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
NetUniv L is non empty set
T is Element of the carrier of L
lim_inf A is Element of the carrier of L
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
A1 is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,A1) is non empty transitive strict directed subnet of A
inf (L,A,A1) is Element of the carrier of L

the carrier of L is non empty set
A is non empty transitive directed NetStr over L
lim_inf A is Element of the carrier of L
the carrier of A is non empty set
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
T is Element of the carrier of L
A1 is non empty transitive directed subnet of A
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
[: the carrier of A1, the carrier of A:] is Relation-like set
bool [: the carrier of A1, the carrier of A:] is set
the mapping of A1 is non empty Relation-like the carrier of A1 -defined the carrier of L -valued Function-like V34( the carrier of A1) V35( the carrier of A1, the carrier of L) Element of bool [: the carrier of A1, the carrier of L:]
[: the carrier of A1, the carrier of L:] is Relation-like set
bool [: the carrier of A1, the carrier of L:] is set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
A9 is non empty Relation-like the carrier of A1 -defined the carrier of A -valued Function-like V34( the carrier of A1) V35( the carrier of A1, the carrier of A) Element of bool [: the carrier of A1, the carrier of A:]
the mapping of A * A9 is non empty Relation-like the carrier of A1 -defined the carrier of L -valued Function-like V34( the carrier of A1) V35( the carrier of A1, the carrier of L) Element of bool [: the carrier of A1, the carrier of L:]
A9 is Element of the carrier of A1
{ (A1 . b1) where b1 is Element of the carrier of A1 : A9 <= b1 } is set
"/\" ( { (A1 . b1) where b1 is Element of the carrier of A1 : A9 <= b1 } ,L) is Element of the carrier of L
x1 is Element of the carrier of A
x is Element of the carrier of A1
x is Element of the carrier of A1
A9 . x is Element of the carrier of A
p is Element of the carrier of A1
A9 . p is Element of the carrier of A
x1 is set
x is Element of the carrier of A
x is Element of the carrier of A1
A9 . x is Element of the carrier of A
p is Element of the carrier of A
p is Element of the carrier of A1
y is Element of the carrier of A1
A9 . y is Element of the carrier of A
A9 . p is Element of the carrier of A

dom x1 is set
rng x1 is set
[: the carrier of A, the carrier of A1:] is Relation-like set
bool [: the carrier of A, the carrier of A1:] is set
x is non empty Relation-like the carrier of A -defined the carrier of A1 -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A1) Element of bool [: the carrier of A, the carrier of A1:]
x is Element of the carrier of A
x . x is Element of the carrier of A1
p is Element of the carrier of A1
p is Element of the carrier of A1
x is non empty Relation-like the carrier of A -defined the carrier of A1 -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A1) Element of bool [: the carrier of A, the carrier of A1:]
A9 * x is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
p is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) Element of bool [: the carrier of A, the carrier of A:]
p is Element of the carrier of A
p . p is Element of the carrier of A
x . p is Element of the carrier of A1
[#] A1 is non empty non proper lower upper Element of bool the carrier of A1
bool the carrier of A1 is set
y is Element of the carrier of A1
A9 . (x . p) is Element of the carrier of A
j is Element of the carrier of A1
p is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,p) is non empty transitive strict directed subnet of A
the carrier of (L,A,p) is non empty set
{ ((L,A,p) . b1) where b1 is Element of the carrier of (L,A,p) : verum } is set
y is set
j is Element of the carrier of (L,A,p)
(L,A,p) . j is Element of the carrier of L
the mapping of (L,A,p) is non empty Relation-like the carrier of (L,A,p) -defined the carrier of L -valued Function-like V34( the carrier of (L,A,p)) V35( the carrier of (L,A,p), the carrier of L) Element of bool [: the carrier of (L,A,p), the carrier of L:]
[: the carrier of (L,A,p), the carrier of L:] is Relation-like set
bool [: the carrier of (L,A,p), the carrier of L:] is set
the mapping of (L,A,p) . j is Element of the carrier of L
the mapping of A * (A9 * x) is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
( the mapping of A * (A9 * x)) . j is set
the mapping of A1 * x is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]
( the mapping of A1 * x) . j is set
x . j is set
the mapping of A1 . (x . j) is set
j1 is Element of the carrier of A
x . j1 is Element of the carrier of A1
A1 . (x . j1) is Element of the carrier of L
the mapping of (L,A,p) is non empty Relation-like the carrier of (L,A,p) -defined the carrier of L -valued Function-like V34( the carrier of (L,A,p)) V35( the carrier of (L,A,p), the carrier of L) Element of bool [: the carrier of (L,A,p), the carrier of L:]
[: the carrier of (L,A,p), the carrier of L:] is Relation-like set
bool [: the carrier of (L,A,p), the carrier of L:] is set
dom the mapping of (L,A,p) is non empty Element of bool the carrier of (L,A,p)
bool the carrier of (L,A,p) is set
rng the mapping of (L,A,p) is non empty Element of bool the carrier of L
bool the carrier of L is set
y is set
j is set
the mapping of (L,A,p) . j is set
j1 is Element of the carrier of (L,A,p)
(L,A,p) . j1 is Element of the carrier of L
y is set
j is Element of the carrier of (L,A,p)
(L,A,p) . j is Element of the carrier of L
the mapping of (L,A,p) . j is Element of the carrier of L
inf (L,A,p) is Element of the carrier of L
//\ ( the mapping of (L,A,p),L) is Element of the carrier of L
"/\" ( { ((L,A,p) . b1) where b1 is Element of the carrier of (L,A,p) : verum } ,L) is Element of the carrier of L
A9 is Element of the carrier of L
x1 is Element of the carrier of A1
{ (A1 . b1) where b1 is Element of the carrier of A1 : x1 <= b1 } is set
"/\" ( { (A1 . b1) where b1 is Element of the carrier of A1 : x1 <= b1 } ,L) is Element of the carrier of L
L is non empty RelStr
NetUniv L is non empty set
the carrier of L is non empty set
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is set
A is Relation-like NetUniv L -defined the carrier of L -valued Element of bool [:(), the carrier of L:]

A1 is non empty transitive directed NetStr over L
A9 is Element of the carrier of L
[A1,A9] is set
{A1,A9} is set
{A1} is set
{{A1,A9},{A1}} is set
x1 is non empty transitive directed subnet of A1
lim_inf x1 is Element of the carrier of L
the carrier of x1 is non empty set
{ ("/\" ( { (x1 . b2) where b2 is Element of the carrier of x1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of x1 : verum } is set
"\/" ( { ("/\" ( { (x1 . b2) where b2 is Element of the carrier of x1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of x1 : verum } ,L) is Element of the carrier of L
A9 is Element of NetUniv L
x is non empty transitive strict directed NetStr over L
A9 is Element of NetUniv L

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
x1 is non empty transitive strict directed NetStr over L
the carrier of x1 is non empty set

A1 is set
A9 is set
[A1,A9] is set
{A1,A9} is set
{A1} is set
{{A1,A9},{A1}} is set
[:(), the carrier of L:] is Relation-like set

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
x1 is non empty transitive strict directed NetStr over L
the carrier of x1 is non empty set
A9 is Element of the carrier of L
x is non empty transitive directed subnet of x1
lim_inf x is Element of the carrier of L
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,L)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,L)) where b1 is Element of the carrier of x : verum } ,L) is Element of the carrier of L

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
x1 is non empty transitive strict directed NetStr over L
the carrier of x1 is non empty set
A9 is Element of the carrier of L
x is non empty transitive directed subnet of x1
lim_inf x is Element of the carrier of L
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,L)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,L)) where b1 is Element of the carrier of x : verum } ,L) is Element of the carrier of L

the carrier of L is non empty set
NetUniv L is non empty set
(L) is Relation-like Convergence-Class of L
A is non empty transitive directed NetStr over L
T is Element of the carrier of L
[A,T] is set
{A,T} is set
{A} is set
{{A,T},{A}} is set
A1 is non empty transitive directed subnet of A
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
A1 is non empty transitive directed subnet of A
inf A1 is Element of the carrier of L
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
A1 is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,A1) is non empty transitive strict directed subnet of A
inf (L,A,A1) is Element of the carrier of L
lim_inf A is Element of the carrier of L
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
A1 is non empty transitive directed subnet of A
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
L is non empty RelStr
A is non empty transitive directed constant NetStr over L
the_value_of A is Element of the carrier of L
the carrier of L is non empty set
T is non empty transitive directed subnet of A
the_value_of T is Element of the carrier of L
the carrier of T is non empty set
the carrier of A is non empty set
[: the carrier of T, the carrier of A:] is Relation-like set
bool [: the carrier of T, the carrier of A:] is set
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( 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 Relation-like set
bool [: the carrier of T, the carrier of L:] is set
the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like constant V34( the carrier of A) V35( 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 Relation-like set
bool [: the carrier of A, the carrier of L:] is set
A1 is non empty Relation-like the carrier of T -defined the carrier of A -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of A) Element of bool [: the carrier of T, the carrier of A:]
the mapping of A * A1 is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
dom the mapping of T is non empty Element of bool the carrier of T
bool the carrier of T is set
the Element of dom the mapping of T is Element of dom the mapping of T
dom the mapping of A is non empty Element of bool the carrier of A
bool the carrier of A is set
the_value_of the mapping of A is set
A1 . the Element of dom the mapping of T is Element of the carrier of A
the mapping of A . (A1 . the Element of dom the mapping of T) is Element of the carrier of L
the mapping of T . the Element of dom the mapping of T is Element of the carrier of L
dom A1 is non empty Element of bool the carrier of T
A9 is set
x1 is set
the mapping of T . A9 is set
the mapping of T . x1 is set
A1 . A9 is set
rng A1 is non empty Element of bool the carrier of A
A1 . x1 is set
the mapping of A . (A1 . A9) is set
the mapping of A . (A1 . x1) is set
the_value_of the mapping of T is set
L is non empty RelStr
(L) is Relation-like Convergence-Class 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 set
bool (bool the carrier of ()) is set
the carrier of L is non empty set
bool the carrier of L is set
bool (bool the carrier of L) is set

(L) is Relation-like Convergence-Class of L
A is non empty transitive directed constant NetStr over L
NetUniv L is non empty set
the_value_of A is Element of the carrier of L
the carrier of L is non empty set
[A,()] is set
{A,()} is set
{A} is set
{{A,()},{A}} is set
T is non empty transitive directed subnet of A
lim_inf T is Element of the carrier of L
the carrier of T is non empty set
{ ("/\" ( { (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
"\/" ( { ("/\" ( { (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
the_value_of T is Element of the carrier of L
L is non empty RelStr
(L) is Relation-like Convergence-Class of L
A is non empty transitive directed NetStr over L
NetUniv L is non empty set
the carrier of L is non empty set
T is non empty transitive directed subnet of A
A1 is Element of the carrier of L
[A,A1] is set
{A,A1} is set
{A} is set
{{A,A1},{A}} is set
[T,A1] is set
{T,A1} is set
{T} is set
{{T,A1},{T}} is set
[:(), the carrier of L:] is Relation-like set
A9 is non empty transitive directed subnet of T
lim_inf A9 is Element of the carrier of L
the carrier of A9 is non empty set
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L
A9 is non empty transitive directed subnet of A
lim_inf A9 is Element of the carrier of L
the carrier of A9 is non empty set
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L

(L) is Relation-like Convergence-Class of L
the carrier of L is non empty set
A is non empty transitive directed NetStr over L
NetUniv L is non empty set
T is Element of the carrier of L
[A,T] is set
{A,T} is set
{A} is set
{{A,T},{A}} is set

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
lim_inf A is Element of the carrier of L
the carrier of A is non empty set
{ ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } is set
"\/" ( { ("/\" ( { (A . b2) where b2 is Element of the carrier of A : b1 <= b2 } ,L)) where b1 is Element of the carrier of A : verum } ,L) is Element of the carrier of L
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is set
A1 is non empty transitive directed subnet of A
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
[:(), the carrier of L:] is Relation-like set
A1 is non empty transitive directed subnet of A
A9 is non empty transitive directed subnet of A1
[A9,T] is set
{A9,T} is set
{A9} is set
{{A9,T},{A9}} is set
lim_inf A9 is Element of the carrier of L
the carrier of A9 is non empty set
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L

A1 is non empty transitive strict directed NetStr over L
the carrier of A1 is non empty set
A1 is non empty transitive directed subnet of A
A9 is non empty transitive directed subnet of A1
[A9,T] is set
{A9,T} is set
{A9} is set
{{A9,T},{A9}} is set
A9 is non empty transitive strict directed NetStr over L
the carrier of A9 is non empty set
lim_inf A9 is Element of the carrier of L
the carrier of A9 is non empty set
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L
A9 is non empty transitive directed subnet of A1
[A9,T] is set
{A9,T} is set
{A9} is set
{{A9,T},{A9}} is set
A1 is non empty transitive directed subnet of A
inf A1 is Element of the carrier of L
A1 is non empty transitive directed subnet of A
inf A1 is Element of the carrier of L
A9 is non empty transitive directed subnet of A1
[A9,T] is set
{A9,T} is set
{A9} is set
{{A9,T},{A9}} is set
lim_inf A1 is Element of the carrier of L
the carrier of A1 is non empty set
{ ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } is set
"\/" ( { ("/\" ( { (A1 . b2) where b2 is Element of the carrier of A1 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A1 : verum } ,L) is Element of the carrier of L
lim_inf A9 is Element of the carrier of L
the carrier of A9 is non empty set
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L
A9 is non empty transitive directed subnet of A1
[A9,T] is set
{A9,T} is set
{A9} is set
{{A9,T},{A9}} is set
A1 is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like V34( the carrier of A) V35( the carrier of A, the carrier of A) (A) Element of bool [: the carrier of A, the carrier of A:]
(L,A,A1) is non empty transitive strict directed subnet of A
inf (L,A,A1) is Element of the carrier of L
L is non empty RelStr
(L) is Relation-like Convergence-Class of L
NetUniv L is non empty set
A is set
T is set
[A,T] is set
{A,T} is set
{A} is set
{{A,T},{A}} is set
the carrier of L is non empty set
[:(), the carrier of L:] is Relation-like set
L is non empty 1-sorted

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

the topology of () is Element of bool (bool the carrier of ())
the carrier of () is non empty set
bool the carrier of () is set
bool (bool the carrier of ()) is set
A1 is set
the carrier of L is non empty set
bool the carrier of L is 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 T or b3 is_eventually_in b1 ) )
}
is set

A9 is Element of bool the carrier of L
A9 is Element of the carrier of L
x1 is non empty transitive directed NetStr over L
[x1,A9] is set
{x1,A9} is set
{x1} is set
{{x1,A9},{x1}} is 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 A or b3 is_eventually_in b1 ) )
}
is set

A9 is Element of bool the carrier of L
L is non empty reflexive RelStr
(L) is Relation-like Convergence-Class of L

A is set
T is set
[A,T] is set
{A,T} is set
{A} is set
{{A,T},{A}} is set
NetUniv L is non empty set
the carrier of L is non empty set
[:(), the carrier of L:] is Relation-like set

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
A9 is non empty transitive strict directed NetStr over L
the carrier of A9 is non empty set
A1 is Element of the carrier of L
lim_inf A9 is Element of the carrier of L
{ ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } is set
"\/" ( { ("/\" ( { (A9 . b2) where b2 is Element of the carrier of A9 : b1 <= b2 } ,L)) where b1 is Element of the carrier of A9 : verum } ,L) is Element of the carrier of L
L is set
A is set

L is non empty reflexive transitive RelStr
the carrier of L is non empty set
bool the carrier of L is set
NetUniv L is non empty set
A is non empty directed Element of bool the carrier of L

the_transitive-closure_of the carrier of L is V9() set
Tarski-Class () is V9() subset-closed Tarski set
the carrier of () is non empty set

the carrier of L is non empty set
bool the carrier of L is set
A is non empty directed Element of bool the carrier of L

"\/" (A,L) is Element of the carrier of L
T is non empty transitive directed subnet of Net-Str A
inf T is Element of the carrier of L
the carrier of T is non empty set
the Element of the carrier of T is Element of the carrier of T
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( 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 Relation-like set
bool [: the carrier of T, the carrier of L:] is set
the carrier of () is non empty set
[: the carrier of T, the carrier of ():] is Relation-like set
bool [: the carrier of T, the carrier of ():] is set
the mapping of () is non empty Relation-like the carrier of () -defined the carrier of L -valued Function-like V34( the carrier of ()) V35( 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 Relation-like set
bool [: the carrier of (), the carrier of L:] is set
A9 is non empty Relation-like the carrier of T -defined the carrier of () -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of ()) Element of bool [: the carrier of T, the carrier of ():]
the mapping of () * A9 is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]
dom the mapping of T is non empty Element of bool the carrier of T
bool the carrier of T is set
the mapping of T . the Element of the carrier of T is Element of the carrier of L
rng the mapping of T is non empty Element of bool the carrier of L
"/\" ((rng the mapping of T),L) is Element of the carrier of L
A9 . the Element of the carrier of T is Element of the carrier of ()
id A is non empty Relation-like A -defined A -valued Function-like one-to-one V34(A) V35(A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is set
(id A) . (A9 . the Element of the carrier of T) is set
the mapping of () . (A9 . the Element of the carrier of T) is Element of the carrier of L
//\ ( the mapping of T,L) is Element of the carrier of L
lim_inf () is Element of the carrier of L
the carrier of () is non empty set
{ ("/\" ( { (() . b2) where b2 is Element of the carrier of () : b1 <= b2 } ,L)) where b1 is Element of the carrier of () : verum } is set
"\/" ( { ("/\" ( { (() . b2) where b2 is Element of the carrier of () : b1 <= b2 } ,L)) where b1 is Element of the carrier of () : verum } ,L) is Element of the carrier of L
[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] is set
T is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V34( the carrier of ()) V35( the carrier of (), the carrier of ()) ( Net-Str A) Element of bool [: the carrier of (), the carrier of ():]
(L,(),T) is non empty transitive strict directed subnet of Net-Str A
inf (L,(),T) is Element of the carrier of L
T is non empty transitive directed subnet of Net-Str A
lim_inf T is Element of the carrier of L
the carrier of T is non empty set
{ ("/\" ( { (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
"\/" ( { ("/\" ( { (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

the carrier of L is non empty set
bool the carrier of L is set
(L) is Relation-like Convergence-Class of L
A is non empty directed Element of bool the carrier of L

"\/" (A,L) is Element of the carrier of L
[(),("\/" (A,L))] is set
{(),("\/" (A,L))} is set
{()} is set
{{(),("\/" (A,L))},{()}} is set
NetUniv L is non empty set
T is non empty transitive directed subnet of Net-Str A
lim_inf T is Element of the carrier of L
the carrier of T is non empty set
{ ("/\" ( { (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
"\/" ( { ("/\" ( { (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

the carrier of L is non empty set
bool the carrier of L is set
(L) is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is set
(L) is Relation-like Convergence-Class 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 set
bool (bool the carrier of ()) is set
A is Element of bool the carrier of L
{ 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 (L) or b3 is_eventually_in b1 ) )
}
is set

T is non empty directed Element of bool the carrier of L
"\/" (T,L) is Element of the carrier of L

[(),("\/" (T,L))] is set
{(),("\/" (T,L))} is set
{()} is set
{{(),("\/" (T,L))},{()}} is set
A1 is Element of bool the carrier of L
the carrier of () is non empty set
A1 is Element of the carrier of ()
A9 is Element of the carrier of L
A9 is Element of the carrier of L
x1 is Element of the carrier of L
x is Element of the carrier of ()
x is Element of the carrier of ()
() . x 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 V34( the carrier of ()) V35( 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 Relation-like set
bool [: the carrier of (), the carrier of L:] is set
the mapping of () . x is Element of the carrier of L
id T is non empty Relation-like T -defined T -valued Function-like one-to-one V34(T) V35(T,T) Element of bool [:T,T:]
[:T,T:] is Relation-like set
bool [:T,T:] is set
(id T) . x is set
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is set
sigma L is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is set

the topology of is Element of bool (bool the carrier of )
the carrier of is non empty set
bool the carrier of is set
bool (bool the carrier of ) is set
(L) is Element of bool (bool the carrier of L)
(L) is Relation-like Convergence-Class 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 set
bool (bool the carrier of ()) is set
A is Element of bool the carrier of L

the carrier of L is non empty set
bool the carrier of L is set
(L) is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is set
(L) is Relation-like Convergence-Class 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 set
bool (bool the carrier of ()) is set
sigma 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 set
bool (bool the carrier of ) is set
A is Element of bool the carrier of L

[::] is Relation-like set
bool [::] is 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 Relation-like set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

the topology of the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete TopSpace-like with_suprema with_infima complete Scott TopAugmentation of L is Element of bool ()
bool () is set

the carrier of L is non empty set
bool the carrier of L is set
(L) is Element of bool (bool the carrier of L)
bool (bool the carrier of L) is set
(L) is Relation-like Convergence-Class 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 set
bool (bool the carrier of ()) is set
A is Element of bool the carrier of L
A ` is Element of bool the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

[::] is Relation-like set
bool [::] is set

A1 is lower Element of bool the carrier of L
A1 ` is upper Element of bool the carrier of L

sigma 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 set
bool (bool the carrier of ) is set
the topology of the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete TopSpace-like with_suprema with_infima complete Scott TopAugmentation of L is Element of bool ()
bool () is set

the topology of the non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete TopSpace-like with_suprema with_infima complete Scott TopAugmentation of L is Element of bool ()
bool () is set
sigma 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 set
bool (bool the carrier of ) is set