:: WAYBEL32 semantic presentation

K112() is non empty V21() V22() V23() non finite V33() V34() set

bool K112() is non empty non finite set

{} is set

the empty Function-like functional V21() V22() V23() V25() V26() V27() finite V33() V35( {} ) set is empty Function-like functional V21() V22() V23() V25() V26() V27() finite V33() V35( {} ) set

1 is non empty set

{{}} is non empty trivial V35(1) set

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

the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete strict Scott TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete RelStr is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete strict Scott TopAugmentation of the non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete RelStr

R is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete TopRelStr

the carrier of R is non empty trivial finite V35(1) set

{ ((downarrow b

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

bool the carrier of R is non empty set

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

x is set

X is Element of the carrier of R

downarrow X is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

{X} is non empty trivial finite V35(1) directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of R

downarrow {X} is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

(downarrow X) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of R

the carrier of R \ (downarrow X) is set

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

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

D is set

D is Element of the carrier of R

downarrow D is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

{D} is non empty trivial finite V35(1) directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of R

downarrow {D} is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

(downarrow D) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of R

the carrier of R \ (downarrow D) is set

G is set

(downarrow D) /\ D is trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of R

{ the carrier of R} is non empty trivial V35(1) set

D is set

G is Element of the carrier of R

downarrow G is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

{G} is non empty trivial finite V35(1) directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of R

downarrow {G} is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

(downarrow G) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of R

the carrier of R \ (downarrow G) is set

the Element of the carrier of R is Element of the carrier of R

{ the Element of the carrier of R} is non empty trivial finite V35(1) directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of R

downarrow the Element of the carrier of R is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

downarrow { the Element of the carrier of R} is non empty trivial finite V35(1) directed filtered lower upper inaccessible_by_directed_joins property(S) Element of bool the carrier of R

(downarrow the Element of the carrier of R) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of R

the carrier of R \ (downarrow the Element of the carrier of R) is set

X is Element of bool (bool the carrier of R)

FinMeetCl X is Element of bool (bool the carrier of R)

{{}, the carrier of R} is set

D is V69(R) quasi_basis Element of bool (bool the carrier of R)

the non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete strict () TopRelStr is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete strict () TopRelStr

R is non empty TopSpace-like reflexive transitive antisymmetric up-complete () TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

N is Element of bool the carrier of R

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

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

{ ((downarrow b

x is V69(R) quasi_prebasis Element of bool (bool the carrier of R)

FinMeetCl x is Element of bool (bool the carrier of R)

X is V69(R) quasi_basis Element of bool (bool the carrier of R)

UniCl X is Element of bool (bool the carrier of R)

D is Element of bool (bool the carrier of R)

union D is Element of bool the carrier of R

D is Element of the carrier of R

G is Element of the carrier of R

G is set

i is Element of bool (bool the carrier of R)

Intersect i is Element of bool the carrier of R

j1 is set

j2 is Element of the carrier of R

downarrow j2 is non empty directed lower Element of bool the carrier of R

{j2} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {j2} is non empty lower Element of bool the carrier of R

(downarrow j2) ` is upper Element of bool the carrier of R

the carrier of R \ (downarrow j2) is set

R is non empty TopSpace-like reflexive transitive antisymmetric up-complete TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

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

{ ((downarrow b

x is Element of the carrier of R

downarrow x is non empty directed lower Element of bool the carrier of R

{x} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {x} is non empty lower Element of bool the carrier of R

Cl {x} is closed Element of bool the carrier of R

X is set

D is Element of the carrier of R

D is Element of bool the carrier of R

G is Element of the carrier of R

X is set

N is V69(R) quasi_prebasis Element of bool (bool the carrier of R)

(downarrow x) ` is upper Element of bool the carrier of R

the carrier of R \ (downarrow x) is set

D is Element of bool (bool the carrier of R)

[#] R is non empty non proper open dense non boundary lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of R

([#] R) \ (downarrow x) is Element of bool the carrier of R

X is non empty transitive directed eventually-directed NetStr over R

sup X is Element of the carrier of R

the mapping of X is non empty Relation-like the carrier of X -defined the carrier of R -valued Function-like V18( the carrier of X, the carrier of R) Element of bool [: the carrier of X, the carrier of R:]

the carrier of X is non empty set

[: the carrier of X, the carrier of R:] is non empty set

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

\\/ ( the mapping of X,R) is Element of the carrier of R

netmap (X,R) is Relation-like the carrier of X -defined the carrier of R -valued Function-like V18( the carrier of X, the carrier of R) Element of bool [: the carrier of X, the carrier of R:]

rng (netmap (X,R)) is non empty Element of bool the carrier of R

"\/" ((rng (netmap (X,R))),R) is Element of the carrier of R

D is a_neighborhood of x

Int D is open Element of bool the carrier of R

N is V69(R) quasi_prebasis Element of bool (bool the carrier of R)

FinMeetCl N is Element of bool (bool the carrier of R)

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

UniCl (FinMeetCl N) is Element of bool (bool the carrier of R)

D is Element of bool (bool the carrier of R)

union D is Element of bool the carrier of R

G is set

G is Element of bool (bool the carrier of R)

Intersect G is Element of bool the carrier of R

i is Element of bool the carrier of R

j1 is Element of the carrier of R

j1 is set

j2 is Element of the carrier of R

downarrow j2 is non empty directed lower Element of bool the carrier of R

{j2} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {j2} is non empty lower Element of bool the carrier of R

(downarrow j2) ` is upper Element of bool the carrier of R

the carrier of R \ (downarrow j2) is set

"\/" (i,R) is Element of the carrier of R

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

E is set

dom the mapping of X is Element of bool the carrier of X

bool the carrier of X is non empty set

j9 is Element of the carrier of R

E9 is set

the mapping of X . E9 is set

b is Element of the carrier of X

X . b is Element of the carrier of R

the mapping of X . b is Element of the carrier of R

k is Element of the carrier of X

k9 is Element of the carrier of X

Ey9 is Element of the carrier of X

X . Ey9 is Element of the carrier of R

the mapping of X . Ey9 is Element of the carrier of R

j1 is Relation-like Function-like set

dom j1 is set

rng j1 is set

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

bool the carrier of X is non empty set

bool ([#] X) is non empty set

j2 is finite Element of bool ([#] X)

E is Element of the carrier of X

j9 is Element of the carrier of X

X . j9 is Element of the carrier of R

the mapping of X . j9 is Element of the carrier of R

E9 is set

j1 . E9 is set

b is Element of the carrier of X

R is non empty reflexive transitive antisymmetric up-complete RelStr

the non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

R is non empty reflexive transitive antisymmetric up-complete RelStr

N is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

R is non empty reflexive transitive antisymmetric up-complete RelStr

N is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

R is non empty reflexive transitive antisymmetric up-complete RelStr

N is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

R is non empty reflexive transitive antisymmetric up-complete Scott TopRelStr

the carrier of R is non empty set

N is Element of the carrier of R

{N} is non empty trivial V35(1) Element of bool the carrier of R

bool the carrier of R is non empty set

Cl {N} is Element of bool the carrier of R

downarrow N is non empty directed lower Element of bool the carrier of R

downarrow {N} is non empty lower Element of bool the carrier of R

x is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

the carrier of x is non empty set

bool the carrier of x is non empty set

D is Element of bool the carrier of x

D is Element of bool the carrier of x

G is Element of bool the carrier of x

X is Element of bool the carrier of x

R is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr

the carrier of R is non empty set

N is Element of the carrier of R

downarrow N is non empty directed lower Element of bool the carrier of R

bool the carrier of R is non empty set

{N} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {N} is non empty lower Element of bool the carrier of R

Cl {N} is closed Element of bool the carrier of R

x is non empty transitive directed eventually-directed NetStr over R

sup x is Element of the carrier of R

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

the carrier of x is non empty set

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

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

\\/ ( the mapping of x,R) is Element of the carrier of R

rng the mapping of x is non empty Element of bool the carrier of R

"\/" ((rng the mapping of x),R) is Element of the carrier of R

X is a_neighborhood of N

Int X is open upper inaccessible_by_directed_joins Element of bool the carrier of R

netmap (x,R) is Relation-like the carrier of x -defined the carrier of R -valued Function-like V18( the carrier of x, the carrier of R) Element of bool [: the carrier of x, the carrier of R:]

rng (netmap (x,R)) is non empty Element of bool the carrier of R

D is Element of bool the carrier of R

D is set

dom the mapping of x is Element of bool the carrier of x

bool the carrier of x is non empty set

G is Element of the carrier of R

G is set

the mapping of x . G is set

i is Element of the carrier of x

x . i is Element of the carrier of R

the mapping of x . i is Element of the carrier of R

j1 is Element of the carrier of x

j2 is Element of the carrier of x

x . j2 is Element of the carrier of R

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

x is non empty transitive directed eventually-directed NetStr over R

sup x is Element of the carrier of R

X is a_neighborhood of N

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

the carrier of R is non empty set

bool the carrier of R is non empty set

N is non empty transitive directed NetStr over R

the carrier of N is non empty set

{ ("/\" ( { (N . b

x is Element of bool the carrier of R

the Element of the carrier of N is Element of the carrier of N

{ (N . b

"/\" ( { (N . b

D is Element of the carrier of R

D is Element of the carrier of R

G is Element of the carrier of N

{ (N . b

"/\" ( { (N . b

G is Element of the carrier of N

{ (N . b

"/\" ( { (N . b

i is Element of the carrier of N

j1 is Element of the carrier of N

j2 is Element of the carrier of N

E is Element of the carrier of N

{ H

{ H

{ H

N . j2 is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

[: the carrier of N, the carrier of R:] is non empty set

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

the mapping of N . j2 is Element of the carrier of R

N . E is Element of the carrier of R

the mapping of N . E is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

k is Element of the carrier of R

E9 is non empty Element of bool the carrier of R

k9 is non empty Element of bool the carrier of R

Ey9 is non empty Element of bool the carrier of R

e is set

k is Element of the carrier of N

N . k is Element of the carrier of R

the mapping of N . k is Element of the carrier of R

k is Element of the carrier of N

e is set

k is Element of the carrier of N

N . k is Element of the carrier of R

the mapping of N . k is Element of the carrier of R

k is Element of the carrier of N

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

the carrier of R is non empty set

bool the carrier of R is non empty set

N is Element of bool the carrier of R

"/\" (N,R) is Element of the carrier of R

x is Element of the carrier of R

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

N is non empty reflexive transitive directed monotone eventually-directed NetStr over R

lim_inf N is Element of the carrier of R

the carrier of R is non empty set

the carrier of N is non empty set

{ ("/\" ( { (N . b

"\/" ( { ("/\" ( { (N . b

sup N is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

{ H

X is Element of the carrier of N

N . X is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

[: the carrier of N, the carrier of R:] is non empty set

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

the mapping of N . X is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

{ H

bool the carrier of R is non empty set

D is Element of the carrier of R

G is Element of the carrier of N

N . G is Element of the carrier of R

the mapping of N . G is Element of the carrier of R

D is Element of the carrier of R

G is Element of the carrier of N

N . G is Element of the carrier of R

the mapping of N . G is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

[: the carrier of N, the carrier of R:] is non empty set

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

rng the mapping of N is non empty Element of bool the carrier of R

bool the carrier of R is non empty set

{ H

\\/ ( the mapping of N,R) is Element of the carrier of R

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

the carrier of R is non empty set

bool the carrier of R is non empty set

Scott-Convergence R is Relation-like Convergence-Class of R

ConvergenceSpace (Scott-Convergence R) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (Scott-Convergence R)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R)))

the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R))) is non empty set

{ b

( not b

( not [b

X is Element of bool the carrier of R

D is non empty directed Element of bool the carrier of R

"\/" (D,R) is Element of the carrier of R

id D is non empty Relation-like Function-like one-to-one set

dom (id D) is set

rng (id D) is set

[:D, the carrier of R:] is non empty set

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

D is Relation-like D -defined the carrier of R -valued Function-like V18(D, the carrier of R) Element of bool [:D, the carrier of R:]

Net-Str (D,D) is non empty reflexive transitive strict monotone NetStr over R

G is non empty reflexive transitive strict directed monotone eventually-directed NetStr over R

NetUniv R is non empty set

lim_inf G is Element of the carrier of R

the carrier of G is non empty set

{ ("/\" ( { (G . b

"\/" ( { ("/\" ( { (G . b

sup G is Element of the carrier of R

the mapping of G is non empty Relation-like the carrier of G -defined the carrier of R -valued Function-like V18( the carrier of G, the carrier of R) Element of bool [: the carrier of G, the carrier of R:]

[: the carrier of G, the carrier of R:] is non empty set

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

\\/ ( the mapping of G,R) is Element of the carrier of R

rng the mapping of G is non empty Element of bool the carrier of R

"\/" ((rng the mapping of G),R) is Element of the carrier of R

rng D is Element of bool the carrier of R

"\/" ((rng D),R) is Element of the carrier of R

[G,("\/" (D,R))] is set

{G,("\/" (D,R))} is set

{G} is non empty trivial V35(1) set

{{G,("\/" (D,R))},{G}} is set

G is Element of bool the carrier of R

G is Element of the carrier of G

i is Element of the carrier of G

G . i is Element of the carrier of R

the mapping of G . i is Element of the carrier of R

(id D) . i is set

D is Element of the carrier of R

D is Element of the carrier of R

Net-Str D is non empty reflexive transitive antisymmetric strict directed NetStr over R

NetUniv R is non empty set

lim_inf (Net-Str D) is Element of the carrier of R

the carrier of (Net-Str D) is non empty set

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

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

[(Net-Str D),D] is set

{(Net-Str D),D} is set

{(Net-Str D)} is non empty trivial V35(1) set

{{(Net-Str D),D},{(Net-Str D)}} is set

G is Element of bool the carrier of R

D is Element of the carrier of R

G is non empty transitive directed NetStr over R

[G,D] is set

{G,D} is set

{G} is non empty trivial V35(1) set

{{G,D},{G}} is set

NetUniv R is non empty set

[:(NetUniv R), the carrier of R:] is non empty set

the_universe_of the carrier of R is set

G is non empty transitive strict directed NetStr over R

the carrier of G is non empty set

D is Element of the carrier of R

lim_inf G is Element of the carrier of R

the carrier of G is non empty set

{ ("/\" ( { (G . b

"\/" ( { ("/\" ( { (G . b

{ (G . b

"/\" ( { (G . b

{ H

i is Element of bool the carrier of R

j1 is non empty directed Element of bool the carrier of R

"\/" (j1,R) is Element of the carrier of R

j1 /\ X is Element of bool the carrier of R

j2 is Element of the carrier of R

E is Element of the carrier of R

j9 is Element of the carrier of G

{ (G . b

"/\" ( { (G . b

{ H

b is Element of the carrier of G

k is Element of the carrier of G

G . k is Element of the carrier of R

the mapping of G is non empty Relation-like the carrier of G -defined the carrier of R -valued Function-like V18( the carrier of G, the carrier of R) Element of bool [: the carrier of G, the carrier of R:]

[: the carrier of G, the carrier of R:] is non empty set

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

the mapping of G . k is Element of the carrier of R

E9 is Element of bool the carrier of R

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

sigma R is Element of bool (bool the carrier of R)

the carrier of R is non empty set

bool the carrier of R is non empty set

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

Scott-Convergence R is Relation-like Convergence-Class of R

ConvergenceSpace (Scott-Convergence R) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (Scott-Convergence R)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R)))

the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R))) is non empty set

N is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

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

the carrier of N is non empty set

bool the carrier of N is non empty set

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

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

[: the carrier of R, the carrier of R:] is non empty set

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

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

x is Element of bool the carrier of N

X is Element of bool the carrier of R

X is Element of bool the carrier of R

D is non empty directed Element of bool the carrier of R

"\/" (D,R) is Element of the carrier of R

G is Element of the carrier of R

D is Element of bool the carrier of N

"\/" (D,N) is Element of the carrier of N

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

the carrier of R is non empty set

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

[: the carrier of R, the carrier of R:] is non empty set

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

sigma R is Element of bool (bool the carrier of R)

bool the carrier of R is non empty set

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

Scott-Convergence R is Relation-like Convergence-Class of R

ConvergenceSpace (Scott-Convergence R) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (Scott-Convergence R)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R)))

the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R))) is non empty set

TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) is strict TopRelStr

the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) is set

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

[: the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #):] is set

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

RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) is strict RelStr

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

x is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

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

sigma R is Element of bool (bool the carrier of R)

the carrier of R is non empty set

bool the carrier of R is non empty set

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

Scott-Convergence R is Relation-like Convergence-Class of R

ConvergenceSpace (Scott-Convergence R) is non empty strict TopSpace-like TopStruct

the topology of (ConvergenceSpace (Scott-Convergence R)) is Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R)))

the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool the carrier of (ConvergenceSpace (Scott-Convergence R)) is non empty set

bool (bool the carrier of (ConvergenceSpace (Scott-Convergence R))) is non empty set

N is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

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

the carrier of N is non empty set

bool the carrier of N is non empty set

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

x is set

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

[: the carrier of R, the carrier of R:] is non empty set

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

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

X is Element of bool the carrier of R

D is Element of bool the carrier of N

x is set

X is Element of bool the carrier of N

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

[: the carrier of R, the carrier of R:] is non empty set

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

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

D is Element of bool the carrier of R

D is non empty directed Element of bool the carrier of R

"\/" (D,R) is Element of the carrier of R

G is Element of the carrier of R

G is Element of bool the carrier of N

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

R is non empty reflexive transitive antisymmetric up-complete Scott TopRelStr

N is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

the carrier of N is non empty set

x is Element of the carrier of N

X is Element of the carrier of N

D is Element of the carrier of N

{D} is non empty trivial V35(1) Element of bool the carrier of N

bool the carrier of N is non empty set

Cl {D} is closed Element of bool the carrier of N

downarrow D is non empty directed lower Element of bool the carrier of N

downarrow {D} is non empty lower Element of bool the carrier of N

D is Element of the carrier of N

{D} is non empty trivial V35(1) Element of bool the carrier of N

Cl {D} is closed Element of bool the carrier of N

downarrow D is non empty directed lower Element of bool the carrier of N

downarrow {D} is non empty lower Element of bool the carrier of N

{x} is non empty trivial V35(1) Element of bool the carrier of N

Cl {x} is closed Element of bool the carrier of N

{X} is non empty trivial V35(1) Element of bool the carrier of N

Cl {X} is closed Element of bool the carrier of N

R is non empty reflexive transitive antisymmetric up-complete RelStr

N is non empty reflexive transitive antisymmetric up-complete TopAugmentation of R

R is non empty reflexive transitive antisymmetric up-complete RelStr

N is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

the carrier of N is non empty set

bool the carrier of N is non empty set

x is Element of the carrier of N

downarrow x is non empty directed lower Element of bool the carrier of N

{x} is non empty trivial V35(1) Element of bool the carrier of N

downarrow {x} is non empty lower Element of bool the carrier of N

(downarrow x) ` is upper Element of bool the carrier of N

the carrier of N \ (downarrow x) is set

X is upper Element of bool the carrier of N

Int ((downarrow x) `) is open upper inaccessible_by_directed_joins Element of bool the carrier of N

R is non empty reflexive transitive antisymmetric up-complete TopRelStr

N is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

the carrier of N is non empty set

bool the carrier of N is non empty set

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

x is upper Element of bool the carrier of N

{ b

D is Element of bool (bool the carrier of N)

meet D is Element of bool the carrier of N

[#] N is non empty non proper open dense non boundary lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of N

D is set

G is Element of bool the carrier of N

D is set

G is Element of the carrier of N

downarrow G is non empty directed lower Element of bool the carrier of N

{G} is non empty trivial V35(1) Element of bool the carrier of N

downarrow {G} is non empty lower Element of bool the carrier of N

(downarrow G) ` is upper Element of bool the carrier of N

the carrier of N \ (downarrow G) is set

D is Element of bool the carrier of N

G is Element of bool the carrier of N

R is non empty reflexive transitive antisymmetric up-complete Scott TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

N is Element of bool the carrier of R

x is non empty directed Element of bool the carrier of R

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

X is set

D is Element of the carrier of R

D is Element of the carrier of R

x is non empty directed Element of bool the carrier of R

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

X is Element of the carrier of R

R is non empty reflexive transitive antisymmetric up-complete TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

N is non empty directed Element of bool the carrier of R

"\/" (N,R) is Element of the carrier of R

x is Element of the carrier of R

R is non empty reflexive transitive antisymmetric up-complete TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

N is Element of bool the carrier of R

x is non empty directed Element of bool the carrier of R

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

X is Element of the carrier of R

D is Element of the carrier of R

R is non empty finite reflexive transitive antisymmetric up-complete RelStr

the carrier of R is non empty finite set

bool the carrier of R is non empty set

N is finite Element of bool the carrier of R

x is non empty finite directed Element of bool the carrier of R

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

X is finite Element of bool the carrier of R

bool x is non empty set

D is finite Element of bool x

D is Element of the carrier of R

G is Element of the carrier of R

G is Element of the carrier of R

R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete RelStr

N is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott TopAugmentation of R

the carrier of N is non empty set

x is Element of the carrier of N

downarrow x is non empty directed lower property(S) Element of bool the carrier of N

bool the carrier of N is non empty set

{x} is non empty trivial V35(1) Element of bool the carrier of N

downarrow {x} is non empty lower property(S) Element of bool the carrier of N

(downarrow x) ` is upper closed_under_directed_sups Element of bool the carrier of N

the carrier of N \ (downarrow x) is set

X is lower closed_under_directed_sups property(S) Element of bool the carrier of N

X ` is open upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of N

the carrier of N \ X is set

R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete RelStr

N is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott TopAugmentation of R

the carrier of N is non empty set

bool the carrier of N is non empty set

{ ((downarrow b

x is Element of bool the carrier of N

[#] N is non empty non proper open dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of N

([#] N) \ x is Element of bool the carrier of N

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

the carrier of R is non empty set

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

[: the carrier of R, the carrier of R:] is non empty set

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

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

bool the carrier of R is non empty set

x ` is Element of bool the carrier of N

the carrier of N \ x is set

D is directed filtered Element of bool the carrier of R

D is non empty directed Element of bool the carrier of N

"\/" (D,N) is Element of the carrier of N

G is Element of the carrier of N

downarrow G is non empty directed lower property(S) Element of bool the carrier of N

{G} is non empty trivial V35(1) Element of bool the carrier of N

downarrow {G} is non empty lower property(S) Element of bool the carrier of N

G is set

i is Element of the carrier of N

G is set

i is Element of the carrier of N

(downarrow G) ` is upper closed_under_directed_sups Element of bool the carrier of N

the carrier of N \ (downarrow G) is set

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

the carrier of R is non empty set

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

[: the carrier of R, the carrier of R:] is non empty set

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

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

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

bool the carrier of R is non empty set

D is Element of the carrier of N

D is Element of the carrier of N

D is Element of the carrier of N

downarrow D is non empty directed lower property(S) Element of bool the carrier of N

{D} is non empty trivial V35(1) Element of bool the carrier of N

downarrow {D} is non empty lower property(S) Element of bool the carrier of N

(downarrow D) ` is upper closed_under_directed_sups Element of bool the carrier of N

the carrier of N \ (downarrow D) is set

R is non empty reflexive transitive antisymmetric up-complete RelStr

the non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopAugmentation of R

the non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott TopRelStr is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott TopRelStr

R is non empty TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

N is Element of bool the carrier of R

x is Element of the carrier of R

X is Element of the carrier of R

downarrow X is Element of bool the carrier of R

{X} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {X} is Element of bool the carrier of R

Cl {X} is Element of bool the carrier of R

N /\ {X} is Element of bool the carrier of R

D is set

R is non empty TopRelStr

the carrier of R is non empty set

bool the carrier of R is non empty set

x is Element of bool the carrier of R

X is Element of the carrier of R

D is Element of the carrier of R

downarrow X is Element of bool the carrier of R

{X} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {X} is Element of bool the carrier of R

Cl {X} is Element of bool the carrier of R

D is set

N is non empty RelStr

the carrier of N is non empty set

R is non empty 1-sorted

the carrier of R is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

NetStr(# the carrier of N, the InternalRel of N,x #) is non empty strict NetStr over R

X is non empty strict NetStr over R

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 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 R -valued Function-like V18( the carrier of X, the carrier of R) Element of bool [: the carrier of X, the carrier of R:]

[: the carrier of X, the carrier of R:] is non empty set

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

X is non empty strict NetStr over R

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 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 R -valued Function-like V18( the carrier of X, the carrier of R) Element of bool [: the carrier of X, the carrier of R:]

[: the carrier of X, the carrier of R:] is non empty set

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

D is non empty strict NetStr over R

the carrier of D is non empty set

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

[: the carrier of D, the carrier of D:] is non empty set

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

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

the mapping of D is non empty Relation-like the carrier of D -defined the carrier of R -valued Function-like V18( the carrier of D, the carrier of R) Element of bool [: the carrier of D, the carrier of R:]

[: the carrier of D, the carrier of R:] is non empty set

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

N is non empty transitive RelStr

the carrier of N is non empty set

R is non empty 1-sorted

the carrier of R is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,x) is non empty strict NetStr over R

the carrier of (R,N,x) is non empty set

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

[: the carrier of (R,N,x), the carrier of (R,N,x):] is non empty set

bool [: the carrier of (R,N,x), the carrier of (R,N,x):] is non empty set

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

N is non empty directed RelStr

the carrier of N is non empty set

R is non empty 1-sorted

the carrier of R is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,x) is non empty strict NetStr over R

the carrier of (R,N,x) is non empty set

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

[: the carrier of (R,N,x), the carrier of (R,N,x):] is non empty set

bool [: the carrier of (R,N,x), the carrier of (R,N,x):] is non empty set

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

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

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

bool the carrier of N is non empty set

[#] (R,N,x) is non empty non proper lower upper Element of bool the carrier of (R,N,x)

bool the carrier of (R,N,x) is non empty set

R is non empty RelStr

N is non empty directed NetStr over R

the carrier of N is non empty set

the carrier of R is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

{ (N . b

"/\" ( { (N . b

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

X is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,X) is non empty strict directed NetStr over R

D is non empty strict directed NetStr over R

x is non empty strict directed NetStr over R

X is non empty strict directed NetStr over R

D is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,D) is non empty strict directed NetStr over R

D is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,D) is non empty strict directed NetStr over R

D is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,D) is non empty strict directed NetStr over R

D is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,D) is non empty strict directed NetStr over R

G is set

D . G is set

D . G is set

G is Element of the carrier of N

D . G is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

D . G is Element of the carrier of R

R is non empty RelStr

N is non empty transitive directed NetStr over R

(R,N) is non empty strict directed NetStr over R

the carrier of N is non empty set

the carrier of R is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,x) is non empty transitive strict directed NetStr over R

R is non empty RelStr

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed NetStr over R

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

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed NetStr over R

the carrier of (R,N) is non empty set

x is Element of the carrier of (R,N)

X is Element of the carrier of (R,N)

(R,N) . x is Element of the carrier of R

the carrier of R is non empty set

the mapping of (R,N) is non empty Relation-like the carrier of (R,N) -defined the carrier of R -valued Function-like V18( the carrier of (R,N), the carrier of R) Element of bool [: the carrier of (R,N), the carrier of R:]

[: the carrier of (R,N), the carrier of R:] is non empty set

bool [: the carrier of (R,N), the carrier of R:] is non empty set

the mapping of (R,N) . x is Element of the carrier of R

(R,N) . X is Element of the carrier of R

the mapping of (R,N) . X is Element of the carrier of R

the carrier of N is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

D is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,D) is non empty transitive strict directed NetStr over R

the InternalRel of (R,N) is Relation-like the carrier of (R,N) -defined the carrier of (R,N) -valued Element of bool [: the carrier of (R,N), the carrier of (R,N):]

[: the carrier of (R,N), the carrier of (R,N):] is non empty set

bool [: the carrier of (R,N), the carrier of (R,N):] is non empty set

RelStr(# the carrier of (R,N), the InternalRel of (R,N) #) is strict RelStr

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

G is Element of the carrier of N

D is Element of the carrier of N

{ H

{ H

bool the carrier of R is non empty set

j1 is Element of the carrier of N

N . j1 is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

the mapping of N . j1 is Element of the carrier of R

E is Element of the carrier of N

N . E is Element of the carrier of R

the mapping of N . E is Element of the carrier of R

j2 is non empty Element of bool the carrier of R

j9 is non empty Element of bool the carrier of R

E9 is set

b is Element of the carrier of R

k is Element of the carrier of N

N . k is Element of the carrier of R

the mapping of N . k is Element of the carrier of R

k9 is Element of the carrier of N

D . D is Element of the carrier of R

"/\" ( { H

D . G is Element of the carrier of R

"/\" ( { H

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

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

R is non empty RelStr

the carrier of R is non empty set

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed NetStr over R

the mapping of (R,N) is non empty Relation-like the carrier of (R,N) -defined the carrier of R -valued Function-like V18( the carrier of (R,N), the carrier of R) Element of bool [: the carrier of (R,N), the carrier of R:]

the carrier of (R,N) is non empty set

[: the carrier of (R,N), the carrier of R:] is non empty set

bool [: the carrier of (R,N), the carrier of R:] is non empty set

rng the mapping of (R,N) is non empty Element of bool the carrier of R

bool the carrier of R is non empty set

the carrier of N is non empty set

{ ("/\" ( { (N . b

[: the carrier of N, the carrier of R:] is non empty set

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

x is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,x) is non empty transitive strict directed NetStr over R

the InternalRel of (R,N) is Relation-like the carrier of (R,N) -defined the carrier of (R,N) -valued Element of bool [: the carrier of (R,N), the carrier of (R,N):]

[: the carrier of (R,N), the carrier of (R,N):] is non empty set

bool [: the carrier of (R,N), the carrier of (R,N):] is non empty set

RelStr(# the carrier of (R,N), the InternalRel of (R,N) #) is strict RelStr

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

dom x is Element of bool the carrier of N

bool the carrier of N is non empty set

X is set

D is set

x . D is set

D is Element of the carrier of N

x . D is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

X is set

D is Element of the carrier of N

{ (N . b

"/\" ( { (N . b

the mapping of (R,N) . D is set

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

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

sup (R,N) is Element of the carrier of R

the carrier of R is non empty set

lim_inf N is Element of the carrier of R

the carrier of N is non empty set

{ ("/\" ( { (N . b

"\/" ( { ("/\" ( { (N . b

{ (N . b

"/\" ( { (N . b

the mapping of (R,N) is non empty Relation-like the carrier of (R,N) -defined the carrier of R -valued Function-like V18( the carrier of (R,N), the carrier of R) Element of bool [: the carrier of (R,N), the carrier of R:]

the carrier of (R,N) is non empty set

[: the carrier of (R,N), the carrier of R:] is non empty set

bool [: the carrier of (R,N), the carrier of R:] is non empty set

\\/ ( the mapping of (R,N),R) is Element of the carrier of R

rng the mapping of (R,N) is non empty Element of bool the carrier of R

bool the carrier of R is non empty set

"\/" ((rng the mapping of (R,N)),R) is Element of the carrier of R

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

N is non empty transitive directed NetStr over R

the carrier of N is non empty set

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

sup (R,N) is Element of the carrier of R

the carrier of R is non empty set

x is Element of the carrier of N

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

lim_inf (N | x) is Element of the carrier of R

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

{ ("/\" ( { ((N | x) . b

"\/" ( { ("/\" ( { ((N | x) . b

lim_inf N is Element of the carrier of R

{ ("/\" ( { (N . b

"\/" ( { ("/\" ( { (N . b

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

the carrier of R is non empty set

bool the carrier of R is non empty set

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

x is upper Element of bool the carrier of R

the carrier of N is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

X is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,X) is non empty transitive strict directed NetStr over R

the carrier of (R,N) is non empty set

the InternalRel of (R,N) is Relation-like the carrier of (R,N) -defined the carrier of (R,N) -valued Element of bool [: the carrier of (R,N), the carrier of (R,N):]

[: the carrier of (R,N), the carrier of (R,N):] is non empty set

bool [: the carrier of (R,N), the carrier of (R,N):] is non empty set

RelStr(# the carrier of (R,N), the InternalRel of (R,N) #) is strict RelStr

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

D is Element of the carrier of (R,N)

D is Element of the carrier of (R,N)

(R,N) . D is Element of the carrier of R

the mapping of (R,N) is non empty Relation-like the carrier of (R,N) -defined the carrier of R -valued Function-like V18( the carrier of (R,N), the carrier of R) Element of bool [: the carrier of (R,N), the carrier of R:]

[: the carrier of (R,N), the carrier of R:] is non empty set

bool [: the carrier of (R,N), the carrier of R:] is non empty set

the mapping of (R,N) . D is Element of the carrier of R

G is Element of the carrier of N

G is Element of the carrier of N

N . G is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

the mapping of N . G is Element of the carrier of R

{ H

j1 is Element of bool the carrier of R

"/\" (j1,R) is Element of the carrier of R

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

the carrier of R is non empty set

bool the carrier of R is non empty set

N is non empty transitive directed NetStr over R

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

x is lower Element of bool the carrier of R

the carrier of N is non empty set

[: the carrier of N, the carrier of R:] is non empty set

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

X is Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

(R,N,X) is non empty transitive strict directed NetStr over R

the carrier of (R,N) is non empty set

the InternalRel of (R,N) is Relation-like the carrier of (R,N) -defined the carrier of (R,N) -valued Element of bool [: the carrier of (R,N), the carrier of (R,N):]

[: the carrier of (R,N), the carrier of (R,N):] is non empty set

bool [: the carrier of (R,N), the carrier of (R,N):] is non empty set

RelStr(# the carrier of (R,N), the InternalRel of (R,N) #) is strict RelStr

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

[: the carrier of N, the carrier of N:] is non empty set

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

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

D is Element of the carrier of N

D is Element of the carrier of (R,N)

G is Element of the carrier of (R,N)

(R,N) . G is Element of the carrier of R

the mapping of (R,N) is non empty Relation-like the carrier of (R,N) -defined the carrier of R -valued Function-like V18( the carrier of (R,N), the carrier of R) Element of bool [: the carrier of (R,N), the carrier of R:]

[: the carrier of (R,N), the carrier of R:] is non empty set

bool [: the carrier of (R,N), the carrier of R:] is non empty set

the mapping of (R,N) . G is Element of the carrier of R

G is Element of the carrier of N

{ H

j1 is Element of the carrier of N

N . j1 is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

the mapping of N . j1 is Element of the carrier of R

j2 is Element of bool the carrier of R

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

R is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete () TopRelStr

the carrier of R is non empty set

N is non empty transitive directed NetStr over R

lim_inf N is Element of the carrier of R

the carrier of N is non empty set

{ ("/\" ( { (N . b

"\/" ( { ("/\" ( { (N . b

x is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

{ H

bool the carrier of R is non empty set

D is Element of bool the carrier of R

D is non empty directed Element of bool the carrier of R

"\/" (D,R) is Element of the carrier of R

(R,N) is non empty transitive strict directed monotone eventually-directed NetStr over R

sup (R,N) is Element of the carrier of R

G is a_neighborhood of x

G is Element of the carrier of R

downarrow G is non empty directed lower property(S) Element of bool the carrier of R

{G} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {G} is non empty lower property(S) Element of bool the carrier of R

Cl {G} is closed Element of bool the carrier of R

Int G is open Element of bool the carrier of R

G is a_neighborhood of "\/" (D,R)

R is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete () TopRelStr

the carrier of R is non empty set

N is non empty transitive directed eventually-directed NetStr over R

lim_inf N is Element of the carrier of R

the carrier of N is non empty set

{ ("/\" ( { (N . b

"\/" ( { ("/\" ( { (N . b

x is Element of the carrier of R

{ (N . b

"/\" ( { (N . b

{ H

bool the carrier of R is non empty set

D is Element of bool the carrier of R

D is non empty directed Element of bool the carrier of R

"\/" (D,R) is Element of the carrier of R

{("\/" (D,R))} is non empty trivial V35(1) Element of bool the carrier of R

G is Element of bool the carrier of R

G is a_neighborhood of x

i is Element of the carrier of N

j1 is Element of the carrier of N

N . j1 is Element of the carrier of R

the mapping of N is non empty Relation-like the carrier of N -defined the carrier of R -valued Function-like V18( the carrier of N, the carrier of R) Element of bool [: the carrier of N, the carrier of R:]

[: the carrier of N, the carrier of R:] is non empty set

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

the mapping of N . j1 is Element of the carrier of R

j2 is Element of the carrier of N

{ H

j9 is Element of the carrier of N

N . j9 is Element of the carrier of R

the mapping of N . j9 is Element of the carrier of R

E9 is non empty Element of bool the carrier of R

b is Element of the carrier of R

k is Element of the carrier of N

N . k is Element of the carrier of R

the mapping of N . k is Element of the carrier of R

"/\" (E9,R) is Element of the carrier of R

b is Element of the carrier of R

downarrow b is non empty directed lower property(S) Element of bool the carrier of R

{b} is non empty trivial V35(1) Element of bool the carrier of R

downarrow {b} is non empty lower property(S) Element of bool the carrier of R

Cl {b} is closed Element of bool the carrier of R

Cl {("\/" (D,R))} is closed Element of bool the carrier of R

downarrow ("\/" (D,R)) is non empty directed lower property(S) Element of bool the carrier of R

downarrow {("\/" (D,R))} is non empty lower property(S) Element of bool the carrier of R