K37() is set
bool K37() is set
K165() is set
bool K165() is set
K169() is Element of bool K165()
{} is set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set
1 is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
A is Relation-like Function-like set
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_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski 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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
x1 is Relation-like Function-like set
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
[:(NetUniv L), the carrier of L:] is Relation-like set
bool [:(NetUniv L), the carrier of L:] is set
A is Relation-like NetUniv L -defined the carrier of L -valued Element of bool [:(NetUniv L), the carrier of L:]
T is Relation-like Convergence-Class 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_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski set
x1 is non empty transitive strict directed NetStr over L
the carrier of x1 is non empty set
A is Relation-like Convergence-Class of L
T is Relation-like Convergence-Class of L
A1 is set
A9 is set
[A1,A9] is set
{A1,A9} is set
{A1} is set
{{A1,A9},{A1}} is set
[:(NetUniv L), the carrier of L:] is Relation-like set
the_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski 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_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski 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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
ConvergenceSpace (L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (L)) is Element of bool (bool the carrier of (ConvergenceSpace (L)))
the carrier of (ConvergenceSpace (L)) is non empty set
bool the carrier of (ConvergenceSpace (L)) is set
bool (bool the carrier of (ConvergenceSpace (L))) 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 non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
(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,(the_value_of A)] is set
{A,(the_value_of A)} is set
{A} is set
{{A,(the_value_of 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
[:(NetUniv L), 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 non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete V122() continuous with_suprema with_infima complete RelStr
(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_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski 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
[:(NetUniv 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
Scott-Convergence L is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class 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
[:(NetUniv L), the carrier of L:] is Relation-like set
L is non empty 1-sorted
A is Relation-like Convergence-Class of L
T is Relation-like Convergence-Class of L
ConvergenceSpace T is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace T) is Element of bool (bool the carrier of (ConvergenceSpace T))
the carrier of (ConvergenceSpace T) is non empty set
bool the carrier of (ConvergenceSpace T) is set
bool (bool the carrier of (ConvergenceSpace T)) is set
ConvergenceSpace A is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace A) is Element of bool (bool the carrier of (ConvergenceSpace A))
the carrier of (ConvergenceSpace A) is non empty set
bool the carrier of (ConvergenceSpace A) is set
bool (bool the carrier of (ConvergenceSpace A)) 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
Scott-Convergence 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
[:(NetUniv L), the carrier of L:] is Relation-like set
the_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski 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
the_universe_of A is V9() subset-closed Tarski set
the_transitive-closure_of A is V9() set
Tarski-Class (the_transitive-closure_of A) is V9() subset-closed Tarski 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
Net-Str A is non empty reflexive transitive strict directed V85(L) eventually-directed NetStr over L
the_universe_of the carrier of L is V9() subset-closed Tarski set
the_transitive-closure_of the carrier of L is V9() set
Tarski-Class (the_transitive-closure_of the carrier of L) is V9() subset-closed Tarski set
the carrier of (Net-Str A) is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
Net-Str A is non empty reflexive transitive strict directed V85(L) eventually-directed NetStr over 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 (Net-Str A) is non empty set
[: the carrier of T, the carrier of (Net-Str A):] is Relation-like set
bool [: the carrier of T, the carrier of (Net-Str A):] is set
the mapping of (Net-Str A) is non empty Relation-like the carrier of (Net-Str A) -defined the carrier of L -valued Function-like V34( the carrier of (Net-Str A)) V35( the carrier of (Net-Str A), the carrier of L) Element of bool [: the carrier of (Net-Str A), the carrier of L:]
[: the carrier of (Net-Str A), the carrier of L:] is Relation-like set
bool [: the carrier of (Net-Str A), the carrier of L:] is set
A9 is non empty Relation-like the carrier of T -defined the carrier of (Net-Str A) -valued Function-like V34( the carrier of T) V35( the carrier of T, the carrier of (Net-Str A)) Element of bool [: the carrier of T, the carrier of (Net-Str A):]
the mapping of (Net-Str 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:]
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 (Net-Str A)
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 (Net-Str A) . (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 (Net-Str A) is Element of the carrier of L
the carrier of (Net-Str A) is non empty set
{ ("/\" ( { ((Net-Str A) . b2) where b2 is Element of the carrier of (Net-Str A) : b1 <= b2 } ,L)) where b1 is Element of the carrier of (Net-Str A) : verum } is set
"\/" ( { ("/\" ( { ((Net-Str A) . b2) where b2 is Element of the carrier of (Net-Str A) : b1 <= b2 } ,L)) where b1 is Element of the carrier of (Net-Str A) : verum } ,L) is Element of the carrier of L
[: the carrier of (Net-Str A), the carrier of (Net-Str A):] is Relation-like set
bool [: the carrier of (Net-Str A), the carrier of (Net-Str A):] is set
T is non empty Relation-like the carrier of (Net-Str A) -defined the carrier of (Net-Str A) -valued Function-like V34( the carrier of (Net-Str A)) V35( the carrier of (Net-Str A), the carrier of (Net-Str A)) ( Net-Str A) Element of bool [: the carrier of (Net-Str A), the carrier of (Net-Str A):]
(L,(Net-Str A),T) is non empty transitive strict directed subnet of Net-Str A
inf (L,(Net-Str A),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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
Net-Str A is non empty reflexive transitive strict directed V85(L) eventually-directed NetStr over L
"\/" (A,L) is Element of the carrier of L
[(Net-Str A),("\/" (A,L))] is set
{(Net-Str A),("\/" (A,L))} is set
{(Net-Str A)} is set
{{(Net-Str A),("\/" (A,L))},{(Net-Str A)}} 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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
ConvergenceSpace (L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (L)) is Element of bool (bool the carrier of (ConvergenceSpace (L)))
the carrier of (ConvergenceSpace (L)) is non empty set
bool the carrier of (ConvergenceSpace (L)) is set
bool (bool the carrier of (ConvergenceSpace (L))) 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
Net-Str T is non empty reflexive transitive strict directed V85(L) eventually-directed NetStr over L
[(Net-Str T),("\/" (T,L))] is set
{(Net-Str T),("\/" (T,L))} is set
{(Net-Str T)} is set
{{(Net-Str T),("\/" (T,L))},{(Net-Str T)}} is set
A1 is Element of bool the carrier of L
the carrier of (Net-Str T) is non empty set
A1 is Element of the carrier of (Net-Str T)
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 (Net-Str T)
x is Element of the carrier of (Net-Str T)
(Net-Str T) . x is Element of the carrier of L
the mapping of (Net-Str T) is non empty Relation-like the carrier of (Net-Str T) -defined the carrier of L -valued Function-like V34( the carrier of (Net-Str T)) V35( the carrier of (Net-Str T), the carrier of L) Element of bool [: the carrier of (Net-Str T), the carrier of L:]
[: the carrier of (Net-Str T), the carrier of L:] is Relation-like set
bool [: the carrier of (Net-Str T), the carrier of L:] is set
the mapping of (Net-Str T) . 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
Scott-Convergence L is Relation-like Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is set
(L) is Element of bool (bool the carrier of L)
(L) is Relation-like Convergence-Class of L
ConvergenceSpace (L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (L)) is Element of bool (bool the carrier of (ConvergenceSpace (L)))
the carrier of (ConvergenceSpace (L)) is non empty set
bool the carrier of (ConvergenceSpace (L)) is set
bool (bool the carrier of (ConvergenceSpace (L))) is set
A is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
ConvergenceSpace (L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (L)) is Element of bool (bool the carrier of (ConvergenceSpace (L)))
the carrier of (ConvergenceSpace (L)) is non empty set
bool the carrier of (ConvergenceSpace (L)) is set
bool (bool the carrier of (ConvergenceSpace (L))) is set
sigma L is Element of bool (bool the carrier of L)
Scott-Convergence L is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is set
A is Element of bool the carrier of L
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 non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete TopSpace-like with_suprema with_infima complete Scott TopAugmentation of L
the carrier 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 non empty set
the InternalRel 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 Relation-like the carrier 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 -defined the carrier 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 -valued Element of bool [: the carrier 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, the carrier 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:]
[: the carrier 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, the carrier 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 Relation-like set
bool [: the carrier 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, the carrier 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 set
RelStr(# the carrier 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, the InternalRel 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 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 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
bool the carrier 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 set
A1 is Element of bool the carrier 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
A9 is Element of bool the carrier 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
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 the carrier 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)
bool (bool the carrier 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 set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete with_suprema with_infima complete RelStr
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
ConvergenceSpace (L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (L)) is Element of bool (bool the carrier of (ConvergenceSpace (L)))
the carrier of (ConvergenceSpace (L)) is non empty set
bool the carrier of (ConvergenceSpace (L)) is set
bool (bool the carrier of (ConvergenceSpace (L))) is set
A is Element of bool the carrier of L
A ` is Element of bool the carrier of L
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 non empty reflexive transitive antisymmetric lower-bounded upper-bounded V72() up-complete /\-complete TopSpace-like with_suprema with_infima complete Scott TopAugmentation 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
the carrier 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 non empty set
the InternalRel 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 Relation-like the carrier 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 -defined the carrier 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 -valued Element of bool [: the carrier 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, the carrier 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:]
[: the carrier 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, the carrier 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 Relation-like set
bool [: the carrier 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, the carrier 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 set
RelStr(# the carrier 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, the InternalRel 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 strict RelStr
bool the carrier 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 set
A9 is Element of bool the carrier 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
A1 is lower Element of bool the carrier of L
A1 ` is upper Element of bool the carrier of L
A9 is Element of bool the carrier 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
A9 ` is Element of bool the carrier 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
sigma L is Element of bool (bool the carrier of L)
Scott-Convergence L is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) 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 the carrier 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)
bool (bool the carrier 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 set
A9 is Element of bool the carrier 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
A9 ` is Element of bool the carrier 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
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 the carrier 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)
bool (bool the carrier 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 set
sigma L is Element of bool (bool the carrier of L)
Scott-Convergence L is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of L
ConvergenceSpace (Scott-Convergence L) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (Scott-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L)))
the carrier of (ConvergenceSpace (Scott-Convergence L)) is non empty set
bool the carrier of (ConvergenceSpace (Scott-Convergence L)) is set
bool (bool the carrier of (ConvergenceSpace (Scott-Convergence L))) is set