:: WAYBEL33 semantic presentation

K130() is non trivial V11() non finite cardinal limit_cardinal Element of bool K126()

K126() is set

bool K126() is non empty set

K37() is non trivial V11() non finite cardinal limit_cardinal set

bool K37() is non empty non trivial non finite set

bool K130() is non empty non trivial non finite set

2 is non empty set

[:2,2:] is non empty Relation-like set

[:[:2,2:],2:] is non empty Relation-like set

bool [:[:2,2:],2:] is non empty set

{} is set

the empty Relation-like non-empty empty-yielding V11() V15() finite finite-yielding V50() cardinal {} -element set is empty Relation-like non-empty empty-yielding V11() V15() finite finite-yielding V50() cardinal {} -element set

1 is non empty set

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

T is non empty Element of bool the carrier of L

BoolePoset T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset T) is non empty non trivial set

bool the carrier of (BoolePoset T) is non empty set

x is non empty filtered upper Element of bool the carrier of (BoolePoset T)

{ ("/\" (b

"\/" ( { ("/\" (b

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

bool the carrier of L is non empty set

bool the carrier of T is non empty set

x is non empty Element of bool the carrier of L

BoolePoset x is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset x) is non empty non trivial set

bool the carrier of (BoolePoset x) is non empty set

y is non empty Element of bool the carrier of T

BoolePoset y is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset y) is non empty non trivial set

bool the carrier of (BoolePoset y) is non empty set

z is non empty filtered upper Element of bool the carrier of (BoolePoset x)

(L,x,z) is Element of the carrier of L

{ ("/\" (b

"\/" ( { ("/\" (b

x is non empty filtered upper Element of bool the carrier of (BoolePoset y)

(T,y,x) is Element of the carrier of T

{ ("/\" (b

"\/" ( { ("/\" (b

F is set

a is Element of bool the carrier of T

"/\" (a,T) is Element of the carrier of T

bool x is non empty Element of bool (bool x)

bool x is non empty set

bool (bool x) is non empty set

j2 is Element of bool the carrier of L

"/\" (j2,L) is Element of the carrier of L

F is set

a is Element of bool the carrier of L

"/\" (a,L) is Element of the carrier of L

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

j2 is Element of bool the carrier of T

"/\" (j2,T) is Element of the carrier of T

L is non empty TopRelStr

lim_inf-Convergence L is Relation-like Convergence-Class of L

ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct

the topology of L is Element of bool (bool the carrier of L)

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

xi L is Element of bool (bool the carrier of L)

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))

the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set

x is Element of bool (bool the carrier of L)

union x is Element of bool the carrier of L

y is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))

union y is Element of bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))

x is Element of bool the carrier of L

y is Element of bool the carrier of L

x /\ y is Element of bool the carrier of L

L is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr

the carrier of L is non empty set

lim_inf-Convergence L is Relation-like Convergence-Class of L

ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct

the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

T is non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact TopRelStr

the carrier of T is non empty trivial finite 1 -element set

the Element of the carrier of T is Element of the carrier of T

x is non empty trivial finite 1 -element TopSpace-like compact TopStruct

the carrier of x is non empty trivial finite 1 -element set

the topology of L is Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

z is Element of the carrier of x

{z} is non empty trivial finite 1 -element Element of bool the carrier of x

bool the carrier of x is non empty finite V50() set

{{},{z}} is finite set

the topology of x is finite V50() Element of bool (bool the carrier of x)

bool (bool the carrier of x) is non empty finite V50() set

xi L is Element of bool (bool the carrier of L)

the non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact () TopRelStr is non empty trivial finite 1 -element TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V163() connected up-complete /\-complete V212() continuous with_suprema with_infima complete lower compact () TopRelStr

L is non empty 1-sorted

the carrier of L is non empty set

T is non empty 1-sorted

the carrier of T is non empty set

x is NetStr over L

the carrier of x is set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

[: the carrier of x, the carrier of T:] is Relation-like set

bool [: the carrier of x, the carrier of T:] is non empty set

y is Relation-like the carrier of x -defined the carrier of T -valued Function-like V41( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]

NetStr(# the carrier of x, the InternalRel of x,y #) is strict NetStr over T

the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) is set

the InternalRel of NetStr(# the carrier of x, the InternalRel of x,y #) is Relation-like the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -defined the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -valued Element of bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):]

[: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):] is Relation-like set

bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of NetStr(# the carrier of x, the InternalRel of x,y #):] is non empty set

RelStr(# the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the InternalRel of NetStr(# the carrier of x, the InternalRel of x,y #) #) is strict RelStr

the mapping of NetStr(# the carrier of x, the InternalRel of x,y #) is Relation-like the carrier of NetStr(# the carrier of x, the InternalRel of x,y #) -defined the carrier of T -valued Function-like V41( the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T) Element of bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:]

[: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:] is Relation-like set

bool [: the carrier of NetStr(# the carrier of x, the InternalRel of x,y #), the carrier of T:] is non empty set

L is non empty 1-sorted

the carrier of L is non empty set

T is non empty 1-sorted

the carrier of T is non empty set

NetUniv L is non empty set

NetUniv T is non empty set

x is NetStr over L

the carrier of x is set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set

the_transitive-closure_of the carrier of L is V9() set

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

y is non empty transitive strict directed NetStr over L

the carrier of y is non empty set

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of L -valued Function-like V41( the carrier of y, the carrier of L) Element of bool [: the carrier of y, the carrier of L:]

[: the carrier of y, the carrier of L:] is non empty Relation-like set

bool [: the carrier of y, the carrier of L:] is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

z is Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

NetStr(# the carrier of y, the InternalRel of y,z #) is non empty transitive strict directed NetStr over T

the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) is non empty set

the InternalRel of NetStr(# the carrier of y, the InternalRel of y,z #) is Relation-like the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -defined the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -valued Element of bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):]

[: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):] is non empty Relation-like set

bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of NetStr(# the carrier of y, the InternalRel of y,z #):] is non empty set

RelStr(# the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the InternalRel of NetStr(# the carrier of y, the InternalRel of y,z #) #) is strict RelStr

the mapping of NetStr(# the carrier of y, the InternalRel of y,z #) is non empty Relation-like the carrier of NetStr(# the carrier of y, the InternalRel of y,z #) -defined the carrier of T -valued Function-like V41( the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T) Element of bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:]

[: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:] is non empty Relation-like set

bool [: the carrier of NetStr(# the carrier of y, the InternalRel of y,z #), the carrier of T:] is non empty set

L is non empty RelStr

T is non empty RelStr

x is non empty transitive directed NetStr over L

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

y is non empty transitive directed NetStr over T

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the carrier of L is non empty set

the carrier of T is non empty set

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is non empty Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

{ (y . b

{ (x . b

z is Element of the carrier of x

x is Element of the carrier of y

{ (x . b

{ (y . b

y is set

A is Element of the carrier of x

x . A is Element of the carrier of L

the mapping of x . A is Element of the carrier of L

F is Element of the carrier of x

x . F is Element of the carrier of L

the mapping of x . F is Element of the carrier of L

a is Element of the carrier of y

y . a is Element of the carrier of T

the mapping of y . a is Element of the carrier of T

j2 is Element of the carrier of y

L is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty transitive directed NetStr over L

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

y is non empty transitive directed NetStr over T

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is non empty Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

{ (y . b

{ (x . b

{ ("/\" (H

{ ("/\" (H

y is set

A is Element of the carrier of x

{ (x . b

"/\" (H

F is Element of the carrier of y

{ (y . b

a is Element of the carrier of x

{ (x . b

j2 is set

G is Element of the carrier of x

x . G is Element of the carrier of L

the mapping of x . G is Element of the carrier of L

[#] x is non empty non proper lower upper Element of bool the carrier of x

bool the carrier of x is non empty set

j2 is Element of the carrier of x

x . j2 is Element of the carrier of L

the mapping of x . j2 is Element of the carrier of L

bool the carrier of L is non empty set

G is non empty Element of bool the carrier of L

"/\" (H

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty transitive directed NetStr over L

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is non empty Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

lim_inf x is Element of the carrier of L

y is non empty transitive directed NetStr over T

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

lim_inf y is Element of the carrier of T

{ (y . b

{ (x . b

{ ("/\" (H

{ ("/\" (H

"\/" ( { ("/\" (H

"\/" ( { ("/\" (H

y is set

A is Element of the carrier of x

{ (x . b

"/\" ( { (x . b

bool the carrier of L is non empty set

y is Element of bool the carrier of L

L is non empty 1-sorted

the carrier of L is non empty set

T is non empty 1-sorted

the carrier of T is non empty set

x is non empty transitive directed NetStr over L

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is non empty Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

y is non empty transitive directed NetStr over T

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

z is non empty transitive directed subnet of x

the carrier of z is non empty set

the InternalRel of z is Relation-like the carrier of z -defined the carrier of z -valued Element of bool [: the carrier of z, the carrier of z:]

[: the carrier of z, the carrier of z:] is non empty Relation-like set

bool [: the carrier of z, the carrier of z:] is non empty set

RelStr(# the carrier of z, the InternalRel of z #) is strict RelStr

the mapping of z is non empty Relation-like the carrier of z -defined the carrier of L -valued Function-like V41( the carrier of z, the carrier of L) Element of bool [: the carrier of z, the carrier of L:]

[: the carrier of z, the carrier of L:] is non empty Relation-like set

bool [: the carrier of z, the carrier of L:] is non empty set

x is strict NetStr over T

the carrier of x is set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is Relation-like the carrier of x -defined the carrier of T -valued Function-like V41( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]

[: the carrier of x, the carrier of T:] is Relation-like set

bool [: the carrier of x, the carrier of T:] is non empty set

[: the carrier of z, the carrier of x:] is non empty Relation-like set

bool [: the carrier of z, the carrier of x:] is non empty set

A is Relation-like the carrier of z -defined the carrier of x -valued Function-like V41( the carrier of z, the carrier of x) Element of bool [: the carrier of z, the carrier of x:]

the mapping of x * A is Relation-like the carrier of z -defined the carrier of L -valued Function-like Element of bool [: the carrier of z, the carrier of L:]

y is non empty transitive strict directed NetStr over T

the carrier of y is non empty set

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

F is Relation-like the carrier of y -defined the carrier of y -valued Function-like V41( the carrier of y, the carrier of y) Element of bool [: the carrier of y, the carrier of y:]

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

the mapping of y * F is Relation-like the carrier of y -defined the carrier of T -valued Function-like Element of bool [: the carrier of y, the carrier of T:]

a is Element of the carrier of y

j2 is Element of the carrier of x

G is Element of the carrier of z

g is Element of the carrier of y

G is Element of the carrier of y

F . G is Element of the carrier of y

F is Element of the carrier of z

A . F is Element of the carrier of x

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

lim_inf-Convergence L is Relation-like Convergence-Class of L

lim_inf-Convergence T is Relation-like Convergence-Class of T

x is NetStr over L

the carrier of x is set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

y is set

[x,y] is V38() set

{x,y} is finite set

{x} is non empty trivial finite 1 -element set

{{x,y},{x}} is finite V50() set

NetUniv L is non empty set

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

z is set

x is set

[z,x] is V38() set

{z,x} is finite set

{z} is non empty trivial finite 1 -element set

{{z,x},{z}} is finite V50() set

NetUniv T is non empty set

A is non empty transitive strict directed NetStr over T

the carrier of A is non empty set

the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]

[: the carrier of A, the carrier of A:] is non empty Relation-like set

bool [: the carrier of A, the carrier of A:] is non empty set

RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr

the mapping of A is non empty Relation-like the carrier of A -defined the carrier of T -valued Function-like V41( the carrier of A, the carrier of T) Element of bool [: the carrier of A, the carrier of T:]

[: the carrier of A, the carrier of T:] is non empty Relation-like set

bool [: the carrier of A, the carrier of T:] is non empty set

the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set

the_transitive-closure_of the carrier of L is V9() set

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

a is non empty transitive strict directed NetStr over L

the carrier of a is non empty set

F is non empty transitive strict directed NetStr over L

a is non empty transitive directed subnet of A

the carrier of a is non empty set

the InternalRel of a is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty Relation-like set

bool [: the carrier of a, the carrier of a:] is non empty set

RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr

the mapping of a is non empty Relation-like the carrier of a -defined the carrier of T -valued Function-like V41( the carrier of a, the carrier of T) Element of bool [: the carrier of a, the carrier of T:]

[: the carrier of a, the carrier of T:] is non empty Relation-like set

bool [: the carrier of a, the carrier of T:] is non empty set

j2 is non empty transitive strict directed subnet of F

the carrier of j2 is non empty set

the InternalRel of j2 is Relation-like the carrier of j2 -defined the carrier of j2 -valued Element of bool [: the carrier of j2, the carrier of j2:]

[: the carrier of j2, the carrier of j2:] is non empty Relation-like set

bool [: the carrier of j2, the carrier of j2:] is non empty set

RelStr(# the carrier of j2, the InternalRel of j2 #) is strict RelStr

the mapping of j2 is non empty Relation-like the carrier of j2 -defined the carrier of L -valued Function-like V41( the carrier of j2, the carrier of L) Element of bool [: the carrier of j2, the carrier of L:]

[: the carrier of j2, the carrier of L:] is non empty Relation-like set

bool [: the carrier of j2, the carrier of L:] is non empty set

y is Element of the carrier of L

lim_inf j2 is Element of the carrier of L

lim_inf a is Element of the carrier of T

[A,y] is V38() set

{A,y} is finite set

{A} is non empty trivial finite 1 -element set

{{A,y},{A}} is finite V50() set

L is non empty 1-sorted

T is non empty 1-sorted

the carrier of L is non empty set

the carrier of T is non empty set

x is non empty NetStr over L

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the mapping of x is non empty Relation-like the carrier of x -defined the carrier of L -valued Function-like V41( the carrier of x, the carrier of L) Element of bool [: the carrier of x, the carrier of L:]

[: the carrier of x, the carrier of L:] is non empty Relation-like set

bool [: the carrier of x, the carrier of L:] is non empty set

y is non empty NetStr over T

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

z is set

x is Element of the carrier of x

y is Element of the carrier of y

A is Element of the carrier of y

y . A is Element of the carrier of T

the mapping of y . A is Element of the carrier of T

F is Element of the carrier of x

x . F is Element of the carrier of L

the mapping of x . F is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

lim_inf-Convergence L is Relation-like Convergence-Class of L

ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))

the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set

lim_inf-Convergence T is Relation-like Convergence-Class of T

ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))

the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set

x is set

bool the carrier of T is non empty set

{ b

( not b

( not [b

bool the carrier of L is non empty set

{ b

( not b

( not [b

y is Element of bool the carrier of L

x is Element of the carrier of T

z is Element of bool the carrier of T

y is non empty transitive directed NetStr over T

[y,x] is V38() set

{y,x} is finite set

{y} is non empty trivial finite 1 -element set

{{y,x},{y}} is finite V50() set

the carrier of y is non empty set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is non empty Relation-like set

bool [: the carrier of y, the carrier of y:] is non empty set

RelStr(# the carrier of y, the InternalRel of y #) is strict RelStr

the mapping of y is non empty Relation-like the carrier of y -defined the carrier of T -valued Function-like V41( the carrier of y, the carrier of T) Element of bool [: the carrier of y, the carrier of T:]

[: the carrier of y, the carrier of T:] is non empty Relation-like set

bool [: the carrier of y, the carrier of T:] is non empty set

A is non empty transitive strict directed NetStr over L

[A,x] is V38() set

{A,x} is finite set

{A} is non empty trivial finite 1 -element set

{{A,x},{A}} is finite V50() set

the carrier of A is non empty set

the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]

[: the carrier of A, the carrier of A:] is non empty Relation-like set

bool [: the carrier of A, the carrier of A:] is non empty set

RelStr(# the carrier of A, the InternalRel of A #) is strict RelStr

the mapping of A is non empty Relation-like the carrier of A -defined the carrier of L -valued Function-like V41( the carrier of A, the carrier of L) Element of bool [: the carrier of A, the carrier of L:]

[: the carrier of A, the carrier of L:] is non empty Relation-like set

bool [: the carrier of A, the carrier of L:] is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

lim_inf-Convergence L is Relation-like Convergence-Class of L

ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct

lim_inf-Convergence T is Relation-like Convergence-Class of T

ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))

the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set

the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))

the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

xi L is Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

xi T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

lim_inf-Convergence L is Relation-like Convergence-Class of L

ConvergenceSpace (lim_inf-Convergence L) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)))

the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence L)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L))) is non empty set

lim_inf-Convergence T is Relation-like Convergence-Class of T

ConvergenceSpace (lim_inf-Convergence T) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (lim_inf-Convergence T)) is Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)))

the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool the carrier of (ConvergenceSpace (lim_inf-Convergence T)) is non empty set

bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence T))) is non empty set

L is non empty reflexive lower-bounded /\-complete RelStr

T is non empty reflexive lower-bounded TopAugmentation of L

the carrier of T is non empty set

bool the carrier of T is non empty set

x is non empty Element of bool the carrier of T

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

bool the carrier of L is non empty set

y is non empty Element of bool the carrier of L

z is Element of the carrier of L

x is Element of the carrier of T

y is Element of the carrier of T

A is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_infima RelStr

T is non empty reflexive transitive antisymmetric TopAugmentation of L

the carrier of T is non empty set

x is Element of the carrier of T

y is Element of the carrier of T

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

z is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

A is Element of the carrier of T

F is Element of the carrier of T

a is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

xi L is Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty strict TopRelStr

the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty set

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

[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty Relation-like set

bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty set

RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) is strict RelStr

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima TopAugmentation of L

the topology of x is Element of bool (bool the carrier of x)

the carrier of x is non empty set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

xi x is Element of bool (bool the carrier of x)

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

xi L is Element of bool (bool the carrier of L)

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima () TopAugmentation of L

the topology of T is Element of bool (bool the carrier of T)

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

xi T is Element of bool (bool the carrier of T)

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L

x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L

the topology of T is Element of bool (bool the carrier of T)

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

xi T is Element of bool (bool the carrier of T)

the topology of x is Element of bool (bool the carrier of x)

the carrier of x is non empty set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

xi x is Element of bool (bool the carrier of x)

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty Relation-like set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

xi L is Element of bool (bool the carrier of L)

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty strict TopRelStr

the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) is non empty set

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

[: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty Relation-like set

bool [: the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #):] is non empty set

RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) is strict RelStr

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

x is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L

the topology of x is Element of bool (bool the carrier of x)

the carrier of x is non empty set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

xi x is Element of bool (bool the carrier of x)

L is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima RelStr

(L) is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict TopAugmentation of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

T is non empty transitive directed NetStr over L

lim_inf T is Element of the carrier of L

the carrier of L is non empty set

the carrier of T is non empty set

{ (inf (T | b

"\/" ( { (inf (T | b

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

z is set

x is Element of the carrier of T

{ (T . b

"/\" ( { (T . b

F is Element of the carrier of T

T | F is non empty transitive strict directed subnet of T

the mapping of (T | F) is non empty Relation-like the carrier of (T | F) -defined the carrier of L -valued Function-like V41( the carrier of (T | F), the carrier of L) Element of bool [: the carrier of (T | F), the carrier of L:]

the carrier of (T | F) is non empty set

[: the carrier of (T | F), the carrier of L:] is non empty Relation-like set

bool [: the carrier of (T | F), the carrier of L:] is non empty set

rng the mapping of (T | F) is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

a is set

{ ((T | F) . b

j2 is Element of the carrier of (T | F)

(T | F) . j2 is Element of the carrier of L

the mapping of (T | F) . j2 is Element of the carrier of L

{ b

G is Element of the carrier of T

T . G is Element of the carrier of L

the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]

[: the carrier of T, the carrier of L:] is non empty Relation-like set

bool [: the carrier of T, the carrier of L:] is non empty set

the mapping of T . G is Element of the carrier of L

g is Element of the carrier of (T | F)

(T | F) . g is Element of the carrier of L

the mapping of (T | F) . g is Element of the carrier of L

G is Element of the carrier of T

y is Element of the carrier of L

a is Element of the carrier of L

a is set

j2 is Element of the carrier of T

T . j2 is Element of the carrier of L

the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]

[: the carrier of T, the carrier of L:] is non empty Relation-like set

bool [: the carrier of T, the carrier of L:] is non empty set

the mapping of T . j2 is Element of the carrier of L

G is Element of the carrier of T

{ b

g is Element of the carrier of (T | F)

T . G is Element of the carrier of L

the mapping of T . G is Element of the carrier of L

G is Element of the carrier of (T | F)

(T | F) . G is Element of the carrier of L

the mapping of (T | F) . G is Element of the carrier of L

{ ((T | F) . b

a is Element of the carrier of L

a is Element of the carrier of T

T | a is non empty transitive strict directed subnet of T

the mapping of (T | a) is non empty Relation-like the carrier of (T | a) -defined the carrier of L -valued Function-like V41( the carrier of (T | a), the carrier of L) Element of bool [: the carrier of (T | a), the carrier of L:]

the carrier of (T | a) is non empty set

[: the carrier of (T | a), the carrier of L:] is non empty Relation-like set

bool [: the carrier of (T | a), the carrier of L:] is non empty set

rng the mapping of (T | a) is non empty Element of bool the carrier of L

inf (T | a) is Element of the carrier of L

//\ ( the mapping of (T | a),L) is Element of the carrier of L

"/\" ((rng the mapping of (T | a)),L) is Element of the carrier of L

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

z is set

x is Element of the carrier of T

T | x is non empty transitive strict directed subnet of T

inf (T | x) is Element of the carrier of L

{ (T . b

the mapping of (T | x) is non empty Relation-like the carrier of (T | x) -defined the carrier of L -valued Function-like V41( the carrier of (T | x), the carrier of L) Element of bool [: the carrier of (T | x), the carrier of L:]

the carrier of (T | x) is non empty set

[: the carrier of (T | x), the carrier of L:] is non empty Relation-like set

bool [: the carrier of (T | x), the carrier of L:] is non empty set

rng the mapping of (T | x) is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

A is set

{ ((T | x) . b

F is Element of the carrier of (T | x)

(T | x) . F is Element of the carrier of L

the mapping of (T | x) . F is Element of the carrier of L

{ b

a is Element of the carrier of T

T . a is Element of the carrier of L

the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]

[: the carrier of T, the carrier of L:] is non empty Relation-like set

bool [: the carrier of T, the carrier of L:] is non empty set

the mapping of T . a is Element of the carrier of L

j2 is Element of the carrier of (T | x)

(T | x) . j2 is Element of the carrier of L

the mapping of (T | x) . j2 is Element of the carrier of L

G is Element of the carrier of T

A is Element of the carrier of L

//\ ( the mapping of (T | x),L) is Element of the carrier of L

"/\" ((rng the mapping of (T | x)),L) is Element of the carrier of L

F is set

a is Element of the carrier of T

T . a is Element of the carrier of L

the mapping of T is non empty Relation-like the carrier of T -defined the carrier of L -valued Function-like V41( the carrier of T, the carrier of L) Element of bool [: the carrier of T, the carrier of L:]

[: the carrier of T, the carrier of L:] is non empty Relation-like set

bool [: the carrier of T, the carrier of L:] is non empty set

the mapping of T . a is Element of the carrier of L

j2 is Element of the carrier of T

{ b

G is Element of the carrier of (T | x)

T . j2 is Element of the carrier of L

the mapping of T . j2 is Element of the carrier of L

g is Element of the carrier of (T | x)

(T | x) . g is Element of the carrier of L

the mapping of (T | x) . g is Element of the carrier of L

{ ((T | x) . b

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset ([#] L)) is non empty non trivial set

bool the carrier of (BoolePoset ([#] L)) is non empty set

T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))

a_net T is non empty reflexive transitive strict directed NetStr over L

the carrier of (a_net T) is non empty set

x is Element of bool the carrier of L

"/\" (x,L) is Element of the carrier of L

y is Element of the carrier of (a_net T)

y `2 is set

(a_net T) | y is non empty reflexive transitive strict directed subnet of a_net T

inf ((a_net T) | y) is Element of the carrier of L

the mapping of ((a_net T) | y) is non empty Relation-like the carrier of ((a_net T) | y) -defined the carrier of L -valued Function-like V41( the carrier of ((a_net T) | y), the carrier of L) Element of bool [: the carrier of ((a_net T) | y), the carrier of L:]

the carrier of ((a_net T) | y) is non empty set

[: the carrier of ((a_net T) | y), the carrier of L:] is non empty Relation-like set

bool [: the carrier of ((a_net T) | y), the carrier of L:] is non empty set

rng the mapping of ((a_net T) | y) is non empty Element of bool the carrier of L

z is set

x is Element of the carrier of L

y is Element of T

[x,y] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{x,y} is finite set

{x} is non empty trivial finite 1 -element set

{{x,y},{x}} is finite V50() set

{ [b

A is Element of the carrier of (a_net T)

[x,y] `1 is Element of the carrier of L

(a_net T) . A is Element of the carrier of L

the mapping of (a_net T) is non empty Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like V41( the carrier of (a_net T), the carrier of L) Element of bool [: the carrier of (a_net T), the carrier of L:]

[: the carrier of (a_net T), the carrier of L:] is non empty Relation-like set

bool [: the carrier of (a_net T), the carrier of L:] is non empty set

the mapping of (a_net T) . A is Element of the carrier of L

[x,y] `2 is Element of T

A `2 is set

F is Element of the carrier of (a_net T)

{ b

a is Element of the carrier of ((a_net T) | y)

(a_net T) . F is Element of the carrier of L

the mapping of (a_net T) . F is Element of the carrier of L

j2 is Element of the carrier of ((a_net T) | y)

((a_net T) | y) . j2 is Element of the carrier of L

the mapping of ((a_net T) | y) . j2 is Element of the carrier of L

{ (((a_net T) | y) . b

z is set

{ (((a_net T) | y) . b

x is Element of the carrier of ((a_net T) | y)

((a_net T) | y) . x is Element of the carrier of L

the mapping of ((a_net T) | y) . x is Element of the carrier of L

{ [b

{ b

y is Element of the carrier of (a_net T)

y `2 is set

A is Element of the carrier of (a_net T)

A is Element of the carrier of L

F is Element of T

[A,F] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{A,F} is finite set

{A} is non empty trivial finite 1 -element set

{{A,F},{A}} is finite V50() set

[A,F] `1 is Element of the carrier of L

[A,F] `2 is Element of T

(a_net T) . y is Element of the carrier of L

the mapping of (a_net T) is non empty Relation-like the carrier of (a_net T) -defined the carrier of L -valued Function-like V41( the carrier of (a_net T), the carrier of L) Element of bool [: the carrier of (a_net T), the carrier of L:]

[: the carrier of (a_net T), the carrier of L:] is non empty Relation-like set

bool [: the carrier of (a_net T), the carrier of L:] is non empty set

the mapping of (a_net T) . y is Element of the carrier of L

a is Element of the carrier of ((a_net T) | y)

((a_net T) | y) . a is Element of the carrier of L

the mapping of ((a_net T) | y) . a is Element of the carrier of L

y `1 is set

//\ ( the mapping of ((a_net T) | y),L) is Element of the carrier of L

"/\" ((rng the mapping of ((a_net T) | y)),L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset ([#] L)) is non empty non trivial set

bool the carrier of (BoolePoset ([#] L)) is non empty set

T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))

(L,([#] L),T) is Element of the carrier of L

{ ("/\" (b

"\/" ( { ("/\" (b

a_net T is non empty reflexive transitive strict directed NetStr over L

lim_inf (a_net T) is Element of the carrier of L

the carrier of (a_net T) is non empty set

{ (inf ((a_net T) | b

z is set

x is Element of the carrier of (a_net T)

(a_net T) | x is non empty reflexive transitive strict directed subnet of a_net T

inf ((a_net T) | x) is Element of the carrier of L

y is Element of the carrier of (a_net T)

{ [b

A is Element of the carrier of L

F is Element of T

[A,F] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{A,F} is finite set

{A} is non empty trivial finite 1 -element set

{{A,F},{A}} is finite V50() set

j2 is Element of the carrier of (BoolePoset ([#] L))

G is Element of bool the carrier of L

[A,G] is V38() Element of [: the carrier of L,(bool the carrier of L):]

[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set

{A,G} is finite set

{{A,G},{A}} is finite V50() set

[A,G] `2 is Element of bool the carrier of L

"/\" (G,L) is Element of the carrier of L

a is Element of the carrier of (a_net T)

(a_net T) | a is non empty reflexive transitive strict directed subnet of a_net T

inf ((a_net T) | a) is Element of the carrier of L

z is set

x is Element of bool the carrier of L

"/\" (x,L) is Element of the carrier of L

Bottom (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))

y is Element of the carrier of L

A is Element of T

[y,A] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{y,A} is finite set

{y} is non empty trivial finite 1 -element set

{{y,A},{y}} is finite V50() set

{ [b

[y,A] `2 is Element of T

F is Element of the carrier of (a_net T)

(a_net T) | F is non empty reflexive transitive strict directed subnet of a_net T

inf ((a_net T) | F) is Element of the carrier of L

"\/" ( { (inf ((a_net T) | b

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset ([#] L)) is non empty non trivial set

bool the carrier of (BoolePoset ([#] L)) is non empty set

bool the carrier of L is non empty Element of bool (bool the carrier of L)

bool (bool the carrier of L) is non empty set

[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set

T is non empty Element of bool the carrier of (BoolePoset ([#] L))

{ [b

x is set

y is Element of the carrier of L

z is Element of T

[y,z] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{y,z} is finite set

{y} is non empty trivial finite 1 -element set

{{y,z},{y}} is finite V50() set

bool ([#] L) is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset ([#] L)) is non empty non trivial set

bool the carrier of (BoolePoset ([#] L)) is non empty set

NetUniv L is non empty set

T is non empty proper filtered upper Element of bool the carrier of (BoolePoset ([#] L))

a_net T is non empty reflexive transitive strict directed NetStr over L

{ [b

the_universe_of the carrier of L is non empty V9() subset-closed Tarski universal set

the_transitive-closure_of the carrier of L is V9() set

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

z is V9() subset-closed Tarski universal set

bool the carrier of L is non empty Element of bool (bool the carrier of L)

bool (bool the carrier of L) is non empty set

[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set

the carrier of (a_net T) is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete RelStr

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

BoolePoset ([#] L) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete RelStr

the carrier of (BoolePoset ([#] L)) is non empty non trivial set

bool the carrier of (BoolePoset ([#] L)) is non empty set

T is non empty proper filtered upper ultra Element of bool the carrier of (BoolePoset ([#] L))

a_net T is non empty reflexive transitive strict directed V266(L) NetStr over L

the carrier of (a_net T) is non empty set

[: the carrier of (a_net T), the carrier of (a_net T):] is non empty Relation-like set

bool [: the carrier of (a_net T), the carrier of (a_net T):] is non empty set

(L,([#] L),T) is Element of the carrier of L

{ ("/\" (b

"\/" ( { ("/\" (b

x is Relation-like the carrier of (a_net T) -defined the carrier of (a_net T) -valued Function-like V41( the carrier of (a_net T), the carrier of (a_net T)) greater_or_equal_to_id Element of bool [: the carrier of (a_net T), the carrier of (a_net T):]

(a_net T) * x is non empty transitive strict directed subnet of a_net T

inf ((a_net T) * x) is Element of the carrier of L

the mapping of ((a_net T) * x) is non empty Relation-like the carrier of ((a_net T) * x) -defined the carrier of L -valued Function-like V41( the carrier of ((a_net T) * x), the carrier of L) Element of bool [: the carrier of ((a_net T) * x), the carrier of L:]

the carrier of ((a_net T) * x) is non empty set

[: the carrier of ((a_net T) * x), the carrier of L:] is non empty Relation-like set

bool [: the carrier of ((a_net T) * x), the carrier of L:] is non empty set

rng the mapping of ((a_net T) * x) is non empty Element of bool the carrier of L

the Element of T is Element of T

//\ ( the mapping of ((a_net T) * x),L) is Element of the carrier of L

"/\" ((rng the mapping of ((a_net T) * x)),L) is Element of the carrier of L

bool ([#] L) is non empty Element of bool (bool ([#] L))

bool ([#] L) is non empty set

bool (bool ([#] L)) is non empty set

the Element of T \ (rng the mapping of ((a_net T) * x)) is Element of bool the Element of T

bool the Element of T is non empty set

the Element of T /\ (rng the mapping of ((a_net T) * x)) is Element of bool the carrier of L

[: the carrier of ((a_net T) * x), the carrier of (a_net T):] is non empty Relation-like set

bool [: the carrier of ((a_net T) * x), the carrier of (a_net T):] is non empty set

y is Element of the carrier of (BoolePoset ([#] L))

the Element of y is Element of y

Bottom (BoolePoset ([#] L)) is Element of the carrier of (BoolePoset ([#] L))

G is Element of the carrier of L

j2 is Element of T

[G,j2] is V38() Element of [: the carrier of L,T:]

[: the carrier of L,T:] is non empty Relation-like set

{G,j2} is finite set

{G} is non empty trivial finite 1 -element set