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

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

"\/" ( { ("/\" ( { (A . b

A1 is set

A9 is Element of the carrier of A

{ (A . b

"/\" ( { (A . b

bool the carrier of L is set

the Element of the carrier of A is Element of the carrier of A

{ (A . b

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

"/\" ((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 . b

"\/" ( { ("/\" ( { (A . b

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

"\/" ( { ("/\" ( { (A1 . b

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

"\/" ( { ("/\" ( { (A . b

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

"\/" ( { ("/\" ( { (A1 . b

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

"\/" ( { ("/\" ( { (A . b

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

"\/" ( { ("/\" ( { (A . b

[: 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 . b

"\/" ( { ("/\" ( { (A1 . b

[: 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 . b

"/\" ( { (A1 . b

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) . b

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) . b

A9 is Element of the carrier of L

x1 is Element of the carrier of A1

{ (A1 . b

"/\" ( { (A1 . b

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

"\/" ( { ("/\" ( { (x1 . b

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

"\/" ( { ("/\" ( { (x . b

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

"\/" ( { ("/\" ( { (x . b

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

"\/" ( { ("/\" ( { (A1 . b

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

"\/" ( { ("/\" ( { (A . b

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

"\/" ( { ("/\" ( { (A1 . b

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

"\/" ( { ("/\" ( { (T . b

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

"\/" ( { ("/\" ( { (A9 . b

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

"\/" ( { ("/\" ( { (A9 . b

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

"\/" ( { ("/\" ( { (A . b

[: 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 . b

"\/" ( { ("/\" ( { (A1 . b

[:(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 . b

"\/" ( { ("/\" ( { (A9 . b

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

"\/" ( { ("/\" ( { (A9 . b

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

"\/" ( { ("/\" ( { (A1 . b

lim_inf A9 is Element of the carrier of L

the carrier of A9 is non empty set

{ ("/\" ( { (A9 . b

"\/" ( { ("/\" ( { (A9 . b

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

{ b

( not b

( not [b

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

{ b

( not b

( not [b

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

"\/" ( { ("/\" ( { (A9 . b

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) . b

"\/" ( { ("/\" ( { ((Net-Str A) . b

[: 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 . b

"\/" ( { ("/\" ( { (T . b

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

"\/" ( { ("/\" ( { (T . b

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

{ b

( not b

( not [b

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