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 b1) `) where b1 is Element of the carrier of R : verum } is set
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 b1) `) where b1 is Element of the carrier of R : verum } is set
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 b1) `) where b1 is Element of the carrier of R : verum } is set
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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
x is Element of bool the carrier of R
the Element of the carrier of N is Element of the carrier of N
{ (N . b1) where b1 is Element of the carrier of N : the Element of the carrier of N <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : the Element of the carrier of N <= b1 } ,R) is Element of the carrier of R
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 . b1) where b1 is Element of the carrier of N : G <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : G <= b1 } ,R) is Element of the carrier of R
G is Element of the carrier of N
{ (N . b1) where b1 is Element of the carrier of N : G <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : G <= b1 } ,R) is Element of the carrier of R
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
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
{ H1(b1) where b1 is Element of the carrier of N : S2[b1] } is set
{ H1(b1) where b1 is Element of the carrier of N : S3[b1] } is set
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 . b1) where b1 is Element of the carrier of N : j2 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : j2 <= b1 } ,R) is Element of the carrier of R
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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
"\/" ( { ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } ,R) is Element of the carrier of R
sup N is Element of the carrier of R
{ (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } ,R) is Element of the carrier of R
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
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 . b1) where b1 is Element of the carrier of N : X <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : X <= b1 } ,R) is Element of the carrier of R
{ H2(b1) where b1 is Element of the carrier of N : S2[b1] } is set
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
{ H2(b1) where b1 is Element of the carrier of N : S1[b1] } is set
\\/ ( 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
{ b1 where b1 is Element of bool the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over R holds
( not [b3,b2] in Scott-Convergence R or b3 is_eventually_in b1 ) ) } is set
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 . b2) where b2 is Element of the carrier of G : b1 <= b2 } ,R)) where b1 is Element of the carrier of G : verum } is set
"\/" ( { ("/\" ( { (G . b2) where b2 is Element of the carrier of G : b1 <= b2 } ,R)) where b1 is Element of the carrier of G : verum } ,R) is Element of the carrier of R
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) . b2) where b2 is Element of the carrier of (Net-Str D) : b1 <= b2 } ,R)) where b1 is Element of the carrier of (Net-Str D) : verum } is set
"\/" ( { ("/\" ( { ((Net-Str D) . b2) where b2 is Element of the carrier of (Net-Str D) : b1 <= b2 } ,R)) where b1 is Element of the carrier of (Net-Str D) : verum } ,R) is Element of the carrier of R
[(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 . b2) where b2 is Element of the carrier of G : b1 <= b2 } ,R)) where b1 is Element of the carrier of G : verum } is set
"\/" ( { ("/\" ( { (G . b2) where b2 is Element of the carrier of G : b1 <= b2 } ,R)) where b1 is Element of the carrier of G : verum } ,R) is Element of the carrier of R
{ (G . b1) where b1 is Element of the carrier of G : a1 <= b1 } is set
"/\" ( { (G . b1) where b1 is Element of the carrier of G : a1 <= b1 } ,R) is Element of the carrier of R
{ H1(b1) where b1 is Element of the carrier of G : S1[b1] } is set
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 . b1) where b1 is Element of the carrier of G : j9 <= b1 } is set
"/\" ( { (G . b1) where b1 is Element of the carrier of G : j9 <= b1 } ,R) is Element of the carrier of R
{ H2(b1) where b1 is Element of the carrier of G : S2[b1] } is set
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
{ b1 where b1 is Element of bool the carrier of N : S1[b1] } is set
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 b1) `) where b1 is Element of the carrier of N : verum } is set
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 . b1) where b1 is Element of the carrier of N : a1 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } ,R) is Element of 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:]
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 . b1) where b1 is Element of the carrier of N : G <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : G <= b1 } ,R) is Element of the carrier of R
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
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
{ H1(b1) where b1 is Element of the carrier of N : S2[b1] } is set
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
"/\" ( { H1(b1) where b1 is Element of the carrier of N : S2[b1] } ,R) is Element of the carrier of R
D . G is Element of the carrier of R
"/\" ( { H1(b1) where b1 is Element of the carrier of N : S1[b1] } ,R) is Element of the carrier of 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 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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is 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 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 . b1) where b1 is Element of the carrier of N : D <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : D <= b1 } ,R) is Element of the carrier of R
X is set
D is Element of the carrier of N
{ (N . b1) where b1 is Element of the carrier of N : D <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : D <= b1 } ,R) is Element of the carrier of R
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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
"\/" ( { ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } ,R) is Element of the carrier of R
{ (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } ,R) 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) 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) . b2) where b2 is Element of the carrier of (N | x) : b1 <= b2 } ,R)) where b1 is Element of the carrier of (N | x) : verum } is set
"\/" ( { ("/\" ( { ((N | x) . b2) where b2 is Element of the carrier of (N | x) : b1 <= b2 } ,R)) where b1 is Element of the carrier of (N | x) : verum } ,R) is Element of the carrier of R
lim_inf N is Element of the carrier of R
{ ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
"\/" ( { ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } ,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 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
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
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
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is 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
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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
"\/" ( { ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } ,R) is Element of the carrier of R
x is Element of the carrier of R
{ (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } ,R) is Element of the carrier of R
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
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 . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } is set
"\/" ( { ("/\" ( { (N . b2) where b2 is Element of the carrier of N : b1 <= b2 } ,R)) where b1 is Element of the carrier of N : verum } ,R) is Element of the carrier of R
x is Element of the carrier of R
{ (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } is set
"/\" ( { (N . b1) where b1 is Element of the carrier of N : a1 <= b1 } ,R) is Element of the carrier of R
{ H1(b1) where b1 is Element of the carrier of N : S1[b1] } is set
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
{ H2(b1) where b1 is Element of the carrier of N : S2[b1] } is set
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