K215() is set
K219() is non empty non trivial V17() V18() V19() non finite V39() V40() countable denumerable Element of bool K215()
bool K215() is non empty set
K95() is non empty non trivial V17() V18() V19() non finite V39() V40() countable denumerable set
bool K95() is non empty non trivial non finite set
bool K219() is non empty non trivial non finite set
K264() is set
{} is empty Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable set
the empty Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable set is empty Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable set
{{}} is non empty trivial finite V38() V41(1) countable set
1 is non empty V17() V18() V19() V23() finite V39() countable Element of K219()
K242({{}}) is M13({{}})
[:K242({{}}),{{}}:] is set
bool [:K242({{}}),{{}}:] is non empty set
K114(K242({{}}),{{}}) is set
{{},1} is non empty finite V38() countable set
[:1,1:] is non empty finite countable set
bool [:1,1:] is non empty finite V38() countable set
[:[:1,1:],1:] is non empty finite countable set
bool [:[:1,1:],1:] is non empty finite V38() countable set
T is RelStr
the carrier of T is set
S is RelStr
the carrier of S is set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of S
e is Element of the carrier of S
[P,e] is set
{P,e} is non empty finite countable set
{P} is non empty trivial finite V41(1) countable set
{{P,e},{P}} is non empty finite V38() countable set
F2() is non empty set
F1() is non empty set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set
{ F4(b1,b2) where b1 is Element of F2(), b2 is Element of F1() : P1[b2] } is set
B is set
the Element of F2() is Element of F2()
P is Element of F1()
F3(P) is set
F4( the Element of F2(),P) is set
B is set
I is Element of F2()
P is Element of F1()
F4(I,P) is set
F3(P) is set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
B is Element of bool the carrier of T
"/\" (S,T) is Element of the carrier of T
"/\" (B,T) is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
B is Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
T is RelStr
the carrier of T is set
bool the carrier of T is non empty set
S is upper Element of bool the carrier of T
B is directed Element of bool the carrier of T
S /\ B is Element of bool the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
e is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
the Element of the carrier of T is Element of the carrier of T
{ the Element of the carrier of T} is non empty trivial finite V41(1) countable Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is non empty finite countable directed Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
bool S is non empty finite V38() countable set
B is finite countable Element of bool S
I is Element of the carrier of T
P is Element of the carrier of T
P is Element of the carrier of T
0 is empty Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable Element of K219()
{0} is non empty trivial finite V38() V41(1) countable Element of bool K219()
[:{0},{0}:] is non empty finite countable set
bool [:{0},{0}:] is non empty finite V38() countable set
[:K219(),K219():] is non empty non trivial non finite set
[0,0] is Element of [:K219(),K219():]
{0,0} is non empty finite V38() countable set
{0} is non empty trivial finite V38() V41(1) countable set
{{0,0},{0}} is non empty finite V38() countable set
{[0,0]} is non empty trivial Relation-like K219() -defined K219() -valued Function-like constant finite V41(1) countable Element of bool [:K219(),K219():]
bool [:K219(),K219():] is non empty non trivial non finite set
T is Relation-like {0} -defined {0} -valued finite countable Element of bool [:{0},{0}:]
RelStr(# {0},T #) is non empty trivial finite 1 -element strict RelStr
S is non empty RelStr
the carrier of S is non empty set
B is Element of the carrier of S
[B,B] is Element of the carrier of [:S,S:]
[:S,S:] is strict RelStr
the carrier of [:S,S:] is set
{B,B} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,B},{B}} is non empty finite V38() countable set
B is non empty trivial finite 1 -element reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive RelStr
T is finite 1-sorted
the carrier of T is finite countable set
bool the carrier of T is non empty finite V38() countable set
S is finite countable Element of bool the carrier of T
T is RelStr
the carrier of T is set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
{} T is empty Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable directed filtered Element of bool the carrier of T
B is Element of the carrier of T
I is Element of the carrier of T
B is Element of the carrier of T
I is Element of the carrier of T
T is non empty trivial finite 1 -element RelStr
the carrier of T is non empty trivial finite V41(1) countable set
bool the carrier of T is non empty finite V38() countable set
S is trivial finite countable Element of bool the carrier of T
{} T is empty trivial proper Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable directed filtered lower upper Element of bool the carrier of T
[#] T is non empty trivial non proper finite V41(1) countable lower upper Element of bool the carrier of T
B is Element of the carrier of T
{B} is non empty trivial finite V41(1) countable Element of bool the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is Element of bool the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is Element of bool the carrier of T
B is upper Element of bool the carrier of T
I is set
P is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is Element of bool the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is Element of bool the carrier of T
B is lower Element of bool the carrier of T
B ` is upper Element of bool the carrier of T
the carrier of T \ B is set
(downarrow S) ` is Element of bool the carrier of T
the carrier of T \ (downarrow S) is set
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
{} T is empty proper Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable directed filtered lower upper Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
{} T is empty proper Function-like functional V17() V18() V19() V21() V22() V23() finite V38() V39() V41( {} ) countable directed filtered lower upper (T) (T) Element of bool the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is (T) Element of bool the carrier of T
S ` is Element of bool the carrier of T
the carrier of T \ S is set
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
B /\ S is Element of bool the carrier of T
T is non empty finite reflexive transitive antisymmetric with_suprema RelStr
the carrier of T is non empty finite countable set
bool the carrier of T is non empty finite V38() countable set
S is finite countable Element of bool the carrier of T
B is non empty finite countable directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
T is non empty finite reflexive transitive antisymmetric with_suprema TopRelStr
the carrier of T is non empty finite countable set
bool the carrier of T is non empty finite V38() countable set
S is finite countable (T) Element of bool the carrier of T
B is finite countable (T) Element of bool the carrier of T
S is finite countable (T) Element of bool the carrier of T
the non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr is non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr
the carrier of the non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr is non empty trivial finite V41(1) countable set
bool the carrier of the non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr is non empty finite V38() countable set
S is trivial finite countable directed filtered upper ( the non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr ) Element of bool the carrier of the non empty trivial finite 1 -element TopSpace-like discrete V79() V80() V81() reflexive transitive antisymmetric lower-bounded upper-bounded V186() connected up-complete /\-complete V226() with_suprema with_infima complete satisfying_axiom_of_approximation continuous completely-distributive strict TopRelStr
T is non empty reflexive RelStr
[#] T is non empty non proper lower upper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
S is non empty directed Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
S is non empty directed Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
B is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[#] T is non empty non proper lower upper (T) (T) Element of bool the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is (T) Element of bool the carrier of T
S ` is Element of bool the carrier of T
the carrier of T \ S is set
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is (T) Element of bool the carrier of T
S ` is Element of bool the carrier of T
the carrier of T \ S is set
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
(S `) ` is Element of bool the carrier of T
the carrier of T \ (S `) is set
T is non empty reflexive transitive up-complete () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
S ` is Element of bool the carrier of T
the carrier of T \ S is set
B is upper (T) Element of bool the carrier of T
B ` is lower (T) Element of bool the carrier of T
the carrier of T \ B is set
B is lower (T) Element of bool the carrier of T
B ` is upper (T) Element of bool the carrier of T
the carrier of T \ B is set
T is non empty reflexive transitive antisymmetric up-complete TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is non empty lower Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
I is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
Cl {S} is closed Element of bool the carrier of T
downarrow S is non empty directed lower Element of bool the carrier of T
downarrow {S} is non empty lower Element of bool the carrier of T
B is Element of bool the carrier of T
I is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
B is Element of the carrier of T
I is Element of the carrier of T
{I} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
Cl {I} is closed Element of bool the carrier of T
downarrow I is non empty directed lower Element of bool the carrier of T
downarrow {I} is non empty lower Element of bool the carrier of T
P is Element of the carrier of T
{P} is non empty trivial finite V41(1) countable Element of bool the carrier of T
Cl {P} is closed Element of bool the carrier of T
downarrow P is non empty directed lower Element of bool the carrier of T
downarrow {P} is non empty lower Element of bool the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
Cl {S} is closed Element of bool the carrier of T
{B} is non empty trivial finite V41(1) countable Element of bool the carrier of T
Cl {B} is closed Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric up-complete () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is non empty lower Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is non empty lower Element of bool the carrier of T
(downarrow S) ` is upper Element of bool the carrier of T
the carrier of T \ (downarrow S) is set
T is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of the carrier of T
downarrow S is non empty directed lower Element of bool the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {S} is non empty lower Element of bool the carrier of T
(downarrow S) ` is upper Element of bool the carrier of T
the carrier of T \ (downarrow S) is set
B is upper Element of bool the carrier of T
Int ((downarrow S) `) is open Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
S is upper Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : S1[b1] } is set
I is Element of bool (bool the carrier of T)
meet I is Element of bool the carrier of T
[#] T is non empty non proper open dense non boundary directed filtered lower upper (T) (T) Element of bool the carrier of T
P is set
e is Element of bool the carrier of T
P is set
e is Element of the carrier of T
downarrow e is non empty directed lower Element of bool the carrier of T
{e} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {e} is non empty lower Element of bool the carrier of T
(downarrow e) ` is upper Element of bool the carrier of T
the carrier of T \ (downarrow e) is set
P is Element of bool the carrier of T
e is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is set
P is Element of the carrier of T
e is Element of the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
T is non empty reflexive TopRelStr
[#] T is non empty non proper dense lower upper (T) (T) Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
S is non empty directed Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
B is Element of the carrier of T
I is Element of the carrier of T
T is non empty reflexive transitive TopRelStr
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is (T) } is set
[#] T is non empty non proper dense lower upper (T) (T) Element of bool the carrier of T
S is Element of bool (bool the carrier of T)
union S is Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is set
P is Element of bool the carrier of T
e is Element of the carrier of T
x is Element of the carrier of T
S is Element of bool the carrier of T
B is Element of bool the carrier of T
S /\ B is Element of bool the carrier of T
I is Element of bool the carrier of T
P is Element of bool the carrier of T
I /\ P is Element of bool the carrier of T
e is non empty directed Element of bool the carrier of T
"\/" (e,T) is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of T
X is Element of the carrier of T
X is Element of the carrier of T
T is non empty RelStr
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
the carrier of T is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
T is non empty reflexive RelStr
NetUniv T is non empty set
the carrier of T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
bool [:(NetUniv T), the carrier of T:] is non empty set
S is Relation-like NetUniv T -defined the carrier of T -valued Element of bool [:(NetUniv T), the carrier of T:]
B is Relation-like Convergence-Class of T
I is non empty transitive strict directed NetStr over T
P is Element of the carrier of T
[I,P] is set
{I,P} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,P},{I}} is non empty finite V38() countable set
e is non empty transitive strict directed NetStr over T
S is Relation-like Convergence-Class of T
B is Relation-like Convergence-Class of T
I is set
P is set
[I,P] is set
{I,P} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,P},{I}} is non empty finite V38() countable set
[:(NetUniv T), the carrier of T:] is non empty set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
e is non empty transitive strict directed NetStr over T
the carrier of e is non empty set
x is Element of the carrier of T
e is non empty transitive strict directed NetStr over T
the carrier of e is non empty set
x is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
S is non empty transitive directed NetStr over T
B is Element of the carrier of T
I is Element of the carrier of T
downarrow I is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{I} is non empty trivial finite V41(1) countable Element of bool the carrier of T
downarrow {I} is non empty lower Element of bool the carrier of T
(T,S) is Element of the carrier of T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
P is Element of the carrier of S
x is Element of the carrier of T
f is Element of the carrier of T
X is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : X <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : X <= b1 } ,T) is Element of the carrier of T
J is Element of the carrier of S
J is Element of the carrier of S
S . J is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . J is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
S is non empty transitive directed NetStr over T
(T,S) is Element of the carrier of T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
I is Element of the carrier of T
uparrow I is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{I} is non empty trivial finite V41(1) countable Element of bool the carrier of T
uparrow {I} is non empty upper Element of bool the carrier of T
P is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : P <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : P <= b1 } ,T) is Element of the carrier of T
f is Element of the carrier of T
X is Element of the carrier of T
X is Element of the carrier of S
S . X is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . X is Element of the carrier of T
J is Element of the carrier of S
S . J is Element of the carrier of T
the mapping of S . J is Element of the carrier of T
T is non empty reflexive RelStr
S is non empty NetStr over T
the carrier of S is non empty set
netmap (S,T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
B is Element of the carrier of S
I is Element of the carrier of S
S . B is Element of the carrier of T
the mapping of S . B is Element of the carrier of T
S . I is Element of the carrier of T
the mapping of S . I is Element of the carrier of T
B is Element of the carrier of S
I is Element of the carrier of S
(netmap (S,T)) . B is Element of the carrier of T
(netmap (S,T)) . I is Element of the carrier of T
(netmap (S,T)) . B is Element of the carrier of T
S . B is Element of the carrier of T
the mapping of S . B is Element of the carrier of T
(netmap (S,T)) . I is Element of the carrier of T
S . I is Element of the carrier of T
the mapping of S . I is Element of the carrier of T
S is non empty set
T is non empty RelStr
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
[:S,S:] is non empty set
bool [:S,S:] is non empty set
I is Relation-like S -defined S -valued Element of bool [:S,S:]
NetStr(# S,I,B #) is non empty strict NetStr over T
P is non empty strict NetStr over T
the carrier of P is non empty set
the mapping of P is non empty Relation-like the carrier of P -defined the carrier of T -valued Function-like V29( the carrier of P) V30( the carrier of P, the carrier of T) Element of bool [: the carrier of P, the carrier of T:]
[: the carrier of P, the carrier of T:] is non empty set
bool [: the carrier of P, the carrier of T:] is non empty set
e is Element of the carrier of P
x is Element of the carrier of P
P . e is Element of the carrier of T
the mapping of P . e is Element of the carrier of T
P . x is Element of the carrier of T
the mapping of P . x is Element of the carrier of T
f is Element of S
X is Element of S
[f,X] is Element of [:S,S:]
{f,X} is non empty finite countable set
{f} is non empty trivial finite V41(1) countable set
{{f,X},{f}} is non empty finite V38() countable set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
B . f is Element of the carrier of T
B . X is Element of the carrier of T
I is non empty strict NetStr over T
the carrier of I is non empty set
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
[: the carrier of I, the carrier of T:] is non empty set
bool [: the carrier of I, the carrier of T:] is non empty set
P is non empty strict NetStr over T
the carrier of P is non empty set
the mapping of P is non empty Relation-like the carrier of P -defined the carrier of T -valued Function-like V29( the carrier of P) V30( the carrier of P, the carrier of T) Element of bool [: the carrier of P, the carrier of T:]
[: the carrier of P, the carrier of T:] is non empty set
bool [: the carrier of P, the carrier of T:] is non empty set
the InternalRel of I is Relation-like the carrier of I -defined the carrier of I -valued Element of bool [: the carrier of I, the carrier of I:]
[: the carrier of I, the carrier of I:] is non empty set
bool [: the carrier of I, the carrier of I:] is non empty set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
e is set
x is set
[e,x] is set
{e,x} is non empty finite countable set
{e} is non empty trivial finite V41(1) countable set
{{e,x},{e}} is non empty finite V38() countable set
f is Element of the carrier of I
I . f is Element of the carrier of T
the mapping of I . f is Element of the carrier of T
X is Element of the carrier of P
P . X is Element of the carrier of T
the mapping of P . X is Element of the carrier of T
X is Element of the carrier of I
I . X is Element of the carrier of T
the mapping of I . X is Element of the carrier of T
J is Element of the carrier of P
P . J is Element of the carrier of T
the mapping of P . J is Element of the carrier of T
f is Element of the carrier of P
P . f is Element of the carrier of T
the mapping of P . f is Element of the carrier of T
X is Element of the carrier of I
I . X is Element of the carrier of T
the mapping of I . X is Element of the carrier of T
X is Element of the carrier of P
P . X is Element of the carrier of T
the mapping of P . X is Element of the carrier of T
J is Element of the carrier of I
I . J is Element of the carrier of T
the mapping of I . J is Element of the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
S is non empty NetStr over T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
the carrier of S is non empty set
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
rng the mapping of S is Element of bool the carrier of T
bool the carrier of T is non empty set
{ (S . b1) where b1 is Element of the carrier of S : verum } is set
dom the mapping of S is Element of bool the carrier of S
bool the carrier of S is non empty set
I is set
P is set
the mapping of S . P is set
e is Element of the carrier of S
S . e is Element of the carrier of T
the mapping of S . e is Element of the carrier of T
I is set
P is Element of the carrier of S
S . P is Element of the carrier of T
the mapping of S . P is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
S is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
rng B is Element of bool the carrier of T
bool the carrier of T is non empty set
(T,S,B) is non empty strict NetStr over T
the carrier of (T,S,B) is non empty set
P is Element of the carrier of (T,S,B)
e is Element of the carrier of (T,S,B)
the mapping of (T,S,B) is non empty Relation-like the carrier of (T,S,B) -defined the carrier of T -valued Function-like V29( the carrier of (T,S,B)) V30( the carrier of (T,S,B), the carrier of T) Element of bool [: the carrier of (T,S,B), the carrier of T:]
[: the carrier of (T,S,B), the carrier of T:] is non empty set
bool [: the carrier of (T,S,B), the carrier of T:] is non empty set
{ ((T,S,B) . b1) where b1 is Element of the carrier of (T,S,B) : verum } is set
(T,S,B) . P is Element of the carrier of T
the mapping of (T,S,B) . P is Element of the carrier of T
(T,S,B) . e is Element of the carrier of T
the mapping of (T,S,B) . e is Element of the carrier of T
x is Element of the carrier of T
dom B is Element of bool S
bool S is non empty set
f is set
B . f is set
X is Element of the carrier of (T,S,B)
(T,S,B) . X is Element of the carrier of T
the mapping of (T,S,B) . X is Element of the carrier of T
S is non empty set
T is non empty RelStr
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
(T,S,B) is non empty strict NetStr over T
netmap ((T,S,B),T) is non empty Relation-like the carrier of (T,S,B) -defined the carrier of T -valued Function-like V29( the carrier of (T,S,B)) V30( the carrier of (T,S,B), the carrier of T) Element of bool [: the carrier of (T,S,B), the carrier of T:]
the carrier of (T,S,B) is non empty set
[: the carrier of (T,S,B), the carrier of T:] is non empty set
bool [: the carrier of (T,S,B), the carrier of T:] is non empty set
the mapping of (T,S,B) is non empty Relation-like the carrier of (T,S,B) -defined the carrier of T -valued Function-like V29( the carrier of (T,S,B)) V30( the carrier of (T,S,B), the carrier of T) Element of bool [: the carrier of (T,S,B), the carrier of T:]
P is Element of the carrier of (T,S,B)
e is Element of the carrier of (T,S,B)
(netmap ((T,S,B),T)) . P is Element of the carrier of T
(netmap ((T,S,B),T)) . e is Element of the carrier of T
(netmap ((T,S,B),T)) . P is Element of the carrier of T
(T,S,B) . P is Element of the carrier of T
the mapping of (T,S,B) . P is Element of the carrier of T
(netmap ((T,S,B),T)) . e is Element of the carrier of T
(T,S,B) . e is Element of the carrier of T
the mapping of (T,S,B) . e is Element of the carrier of T
S is non empty set
T is non empty transitive RelStr
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
(T,S,B) is non empty strict monotone NetStr over T
the carrier of (T,S,B) is non empty set
P is Element of the carrier of (T,S,B)
e is Element of the carrier of (T,S,B)
x is Element of the carrier of (T,S,B)
(T,S,B) . P is Element of the carrier of T
the mapping of (T,S,B) is non empty Relation-like the carrier of (T,S,B) -defined the carrier of T -valued Function-like V29( the carrier of (T,S,B)) V30( the carrier of (T,S,B), the carrier of T) Element of bool [: the carrier of (T,S,B), the carrier of T:]
[: the carrier of (T,S,B), the carrier of T:] is non empty set
bool [: the carrier of (T,S,B), the carrier of T:] is non empty set
the mapping of (T,S,B) . P is Element of the carrier of T
(T,S,B) . e is Element of the carrier of T
the mapping of (T,S,B) . e is Element of the carrier of T
(T,S,B) . x is Element of the carrier of T
the mapping of (T,S,B) . x is Element of the carrier of T
S is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
(T,S,B) is non empty strict monotone NetStr over T
the carrier of (T,S,B) is non empty set
I is Element of the carrier of (T,S,B)
(T,S,B) . I is Element of the carrier of T
the mapping of (T,S,B) is non empty Relation-like the carrier of (T,S,B) -defined the carrier of T -valued Function-like V29( the carrier of (T,S,B)) V30( the carrier of (T,S,B), the carrier of T) Element of bool [: the carrier of (T,S,B), the carrier of T:]
[: the carrier of (T,S,B), the carrier of T:] is non empty set
bool [: the carrier of (T,S,B), the carrier of T:] is non empty set
the mapping of (T,S,B) . I is Element of the carrier of T
T is non empty transitive RelStr
the carrier of T is non empty set
NetUniv T is non empty set
S is non empty set
[:S, the carrier of T:] is non empty set
bool [:S, the carrier of T:] is non empty set
B is non empty Relation-like S -defined the carrier of T -valued Function-like V29(S) V30(S, the carrier of T) Element of bool [:S, the carrier of T:]
(T,S,B) is non empty transitive strict monotone NetStr over T
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
e is V17() subset-closed Tarski universal set
I is non empty transitive strict directed NetStr over T
the carrier of I is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
id the carrier of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V29( the carrier of T) V30( the carrier of T, the carrier of T) Element of bool [: the carrier of T, the carrier of T:]
S is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V29( the carrier of T) V30( the carrier of T, the carrier of T) Element of bool [: the carrier of T, the carrier of T:]
rng S is Element of bool the carrier of T
bool the carrier of T is non empty set
[#] T is non empty non proper directed filtered lower upper (T) (T) Element of bool the carrier of T
(T, the carrier of T,S) is non empty reflexive transitive strict monotone NetStr over T
B is non empty reflexive transitive strict directed NetStr over T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive directed monotone eventually-directed NetStr over T
(T,S) is Element of the carrier of T
the carrier of T is non empty set
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
sup S is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : a1 <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : a1 <= b1 } ,T) is Element of the carrier of T
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
I is Element of the carrier of S
S . I is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . I is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : I <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : I <= b1 } ,T) is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of S
S . x is Element of the carrier of T
the mapping of S . x is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of S
S . x is Element of the carrier of T
the mapping of S . x is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
rng the mapping of S is Element of bool the carrier of T
bool the carrier of T is non empty set
{ H2(b1) where b1 is Element of the carrier of S : S1[b1] } is set
\\/ ( the mapping of S,T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty transitive directed constant NetStr over T
the_value_of S is Element of the carrier of T
the carrier of T is non empty set
(T,S) is Element of the carrier of T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
the Element of the carrier of S is Element of the carrier of S
S . the Element of the carrier of S is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like constant V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . the Element of the carrier of S is Element of the carrier of T
P is Element of the carrier of T
e is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : e <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : e <= b1 } ,T) is Element of the carrier of T
x is Element of the carrier of S
f is Element of the carrier of S
S . f is Element of the carrier of T
the mapping of S . f is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : x <= b1 } is set
P is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } ,T) is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of S
S . f is Element of the carrier of T
the mapping of S . f is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of S
S . f is Element of the carrier of T
the mapping of S . f is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty transitive directed constant NetStr over T
the_value_of S is Element of the carrier of T
the carrier of T is non empty set
(T,S) is Element of the carrier of T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
"\/" ( { ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } ,T) is Element of the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[S,S] is Element of [: the carrier of T, the carrier of T:]
{S,S} is non empty finite countable set
{S} is non empty trivial finite V41(1) countable set
{{S,S},{S}} is non empty finite V38() countable set
{[S,S]} is non empty trivial Relation-like the carrier of T -defined the carrier of T -valued Function-like constant finite V41(1) countable Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
id {S} is non empty Relation-like {S} -defined {S} -valued Function-like one-to-one V29({S}) V30({S},{S}) finite countable Element of bool [:{S},{S}:]
[:{S},{S}:] is non empty finite countable set
bool [:{S},{S}:] is non empty finite V38() countable set
dom (id {S}) is trivial finite countable Element of bool {S}
bool {S} is non empty finite V38() countable set
rng (id {S}) is trivial finite countable Element of bool {S}
[:{S}, the carrier of T:] is non empty set
bool [:{S}, the carrier of T:] is non empty set
B is Relation-like {S} -defined {S} -valued finite countable Element of bool [:{S},{S}:]
I is non empty Relation-like {S} -defined the carrier of T -valued Function-like V29({S}) V30({S}, the carrier of T) finite countable Element of bool [:{S}, the carrier of T:]
NetStr(# {S},B,I #) is non empty strict NetStr over T
the carrier of NetStr(# {S},B,I #) is non empty set
the InternalRel of NetStr(# {S},B,I #) is Relation-like the carrier of NetStr(# {S},B,I #) -defined the carrier of NetStr(# {S},B,I #) -valued Element of bool [: the carrier of NetStr(# {S},B,I #), the carrier of NetStr(# {S},B,I #):]
[: the carrier of NetStr(# {S},B,I #), the carrier of NetStr(# {S},B,I #):] is non empty set
bool [: the carrier of NetStr(# {S},B,I #), the carrier of NetStr(# {S},B,I #):] is non empty set
the mapping of NetStr(# {S},B,I #) is non empty Relation-like the carrier of NetStr(# {S},B,I #) -defined the carrier of T -valued Function-like V29( the carrier of NetStr(# {S},B,I #)) V30( the carrier of NetStr(# {S},B,I #), the carrier of T) Element of bool [: the carrier of NetStr(# {S},B,I #), the carrier of T:]
[: the carrier of NetStr(# {S},B,I #), the carrier of T:] is non empty set
bool [: the carrier of NetStr(# {S},B,I #), the carrier of T:] is non empty set
B is strict NetStr over T
the carrier of B is set
the InternalRel of B is Relation-like the carrier of B -defined the carrier of B -valued Element of bool [: the carrier of B, the carrier of B:]
[: the carrier of B, the carrier of B:] is set
bool [: the carrier of B, the carrier of B:] is non empty set
the mapping of B is Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is set
bool [: the carrier of B, the carrier of T:] is non empty set
I is strict NetStr over T
the carrier of I is set
the InternalRel of I is Relation-like the carrier of I -defined the carrier of I -valued Element of bool [: the carrier of I, the carrier of I:]
[: the carrier of I, the carrier of I:] is set
bool [: the carrier of I, the carrier of I:] is non empty set
the mapping of I is Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
[: the carrier of I, the carrier of T:] is set
bool [: the carrier of I, the carrier of T:] is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is strict NetStr over T
the carrier of (T,S) is set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is non empty strict NetStr over T
the carrier of (T,S) is non empty set
B is Element of the carrier of (T,S)
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is non empty strict NetStr over T
the carrier of (T,S) is non empty set
B is Element of the carrier of (T,S)
(T,S) . B is Element of the carrier of T
the mapping of (T,S) is non empty Relation-like the carrier of (T,S) -defined the carrier of T -valued Function-like V29( the carrier of (T,S)) V30( the carrier of (T,S), the carrier of T) Element of bool [: the carrier of (T,S), the carrier of T:]
[: the carrier of (T,S), the carrier of T:] is non empty set
bool [: the carrier of (T,S), the carrier of T:] is non empty set
the mapping of (T,S) . B is Element of the carrier of T
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
id {S} is non empty Relation-like {S} -defined {S} -valued Function-like one-to-one V29({S}) V30({S},{S}) finite countable Element of bool [:{S},{S}:]
[:{S},{S}:] is non empty finite countable set
bool [:{S},{S}:] is non empty finite V38() countable set
(id {S}) . B is set
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is non empty strict NetStr over T
the carrier of (T,S) is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
the InternalRel of (T,S) is Relation-like the carrier of (T,S) -defined the carrier of (T,S) -valued Element of bool [: the carrier of (T,S), the carrier of (T,S):]
[: the carrier of (T,S), the carrier of (T,S):] is non empty set
bool [: the carrier of (T,S), the carrier of (T,S):] is non empty set
I is Element of the carrier of (T,S)
[I,I] is Element of the carrier of [:(T,S),(T,S):]
[:(T,S),(T,S):] is strict RelStr
the carrier of [:(T,S),(T,S):] is set
{I,I} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,I},{I}} is non empty finite V38() countable set
{[I,I]} is non empty trivial Function-like finite V41(1) countable set
P is Element of the carrier of (T,S)
P is Element of the carrier of (T,S)
e is Element of the carrier of (T,S)
x is Element of the carrier of (T,S)
P is Element of the carrier of (T,S)
e is Element of the carrier of (T,S)
P is Element of the carrier of (T,S)
e is Element of the carrier of (T,S)
T is non empty 1-sorted
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is non empty reflexive transitive antisymmetric strict directed NetStr over T
B is set
the carrier of (T,S) is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
e is Element of the carrier of (T,S)
(T,S) . e is Element of the carrier of T
the mapping of (T,S) is non empty Relation-like the carrier of (T,S) -defined the carrier of T -valued Function-like V29( the carrier of (T,S)) V30( the carrier of (T,S), the carrier of T) Element of bool [: the carrier of (T,S), the carrier of T:]
[: the carrier of (T,S), the carrier of T:] is non empty set
bool [: the carrier of (T,S), the carrier of T:] is non empty set
the mapping of (T,S) . e is Element of the carrier of T
P is Element of the carrier of (T,S)
e is Element of the carrier of (T,S)
(T,S) . e is Element of the carrier of T
the mapping of (T,S) . e is Element of the carrier of T
T is non empty reflexive antisymmetric RelStr
the carrier of T is non empty set
S is Element of the carrier of T
(T,S) is non empty reflexive transitive antisymmetric strict directed NetStr over T
(T,(T,S)) is Element of the carrier of T
the carrier of (T,S) is non empty set
{ ("/\" ( { ((T,S) . b2) where b2 is Element of the carrier of (T,S) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,S) : verum } is set
"\/" ( { ("/\" ( { ((T,S) . b2) where b2 is Element of the carrier of (T,S) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,S) : verum } ,T) is Element of the carrier of T
P is Element of the carrier of T
{P} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
e is set
x is Element of the carrier of (T,S)
{ ((T,S) . b1) where b1 is Element of the carrier of (T,S) : x <= b1 } is set
"/\" ( { ((T,S) . b1) where b1 is Element of the carrier of (T,S) : x <= b1 } ,T) is Element of the carrier of T
X is set
X is Element of the carrier of (T,S)
(T,S) . X is Element of the carrier of T
the mapping of (T,S) is non empty Relation-like the carrier of (T,S) -defined the carrier of T -valued Function-like V29( the carrier of (T,S)) V30( the carrier of (T,S), the carrier of T) Element of bool [: the carrier of (T,S), the carrier of T:]
[: the carrier of (T,S), the carrier of T:] is non empty set
bool [: the carrier of (T,S), the carrier of T:] is non empty set
the mapping of (T,S) . X is Element of the carrier of T
J is Element of the carrier of (T,S)
(T,S) . J is Element of the carrier of T
the mapping of (T,S) . J is Element of the carrier of T
X is Element of the carrier of (T,S)
(T,S) . x is Element of the carrier of T
the mapping of (T,S) is non empty Relation-like the carrier of (T,S) -defined the carrier of T -valued Function-like V29( the carrier of (T,S)) V30( the carrier of (T,S), the carrier of T) Element of bool [: the carrier of (T,S), the carrier of T:]
[: the carrier of (T,S), the carrier of T:] is non empty set
bool [: the carrier of (T,S), the carrier of T:] is non empty set
the mapping of (T,S) . x is Element of the carrier of T
the Element of the carrier of (T,S) is Element of the carrier of (T,S)
{ ((T,S) . b1) where b1 is Element of the carrier of (T,S) : the Element of the carrier of (T,S) <= b1 } is set
"/\" ( { ((T,S) . b1) where b1 is Element of the carrier of (T,S) : the Element of the carrier of (T,S) <= b1 } ,T) is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
NetUniv T is non empty set
S is Element of the carrier of T
(T,S) is non empty reflexive transitive antisymmetric strict directed NetStr over T
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
the carrier of (T,S) is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
bool the carrier of T is non empty set
P is V17() subset-closed Tarski universal set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
B is Element of bool the carrier of T
the Element of the carrier of S is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } ,T) is Element of the carrier of T
P is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : x <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : x <= b1 } ,T) is Element of the carrier of T
f is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : f <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : f <= b1 } ,T) is Element of the carrier of T
X is Element of the carrier of S
X is Element of the carrier of S
J is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : X <= b1 } is set
{ (S . b1) where b1 is Element of the carrier of S : X <= b1 } is set
{ (S . b1) where b1 is Element of the carrier of S : J <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : J <= b1 } ,T) is Element of the carrier of T
D9 is Element of the carrier of T
E9 is set
x9 is Element of the carrier of S
S . x9 is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . x9 is Element of the carrier of T
X1 is Element of the carrier of S
E9 is set
x9 is Element of the carrier of S
S . x9 is Element of the carrier of T
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S . x9 is Element of the carrier of T
X1 is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
(T) is Relation-like Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
{ b1 where b1 is Element of bool the carrier of T : for b2 being Element of the carrier of T holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over T holds
( not [b3,b2] in (T) or b3 is_eventually_in b1 ) ) } is set
I is Element of bool the carrier of T
P is non empty directed Element of bool the carrier of T
"\/" (P,T) is Element of the carrier of T
id P is non empty Relation-like P -defined P -valued Function-like one-to-one V29(P) V30(P,P) Element of bool [:P,P:]
[:P,P:] is non empty set
bool [:P,P:] is non empty set
dom (id P) is Element of bool P
bool P is non empty set
rng (id P) is Element of bool P
[:P, the carrier of T:] is non empty set
bool [:P, the carrier of T:] is non empty set
e is non empty Relation-like P -defined the carrier of T -valued Function-like V29(P) V30(P, the carrier of T) Element of bool [:P, the carrier of T:]
(T,P,e) is non empty reflexive transitive strict monotone NetStr over T
x is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
NetUniv T is non empty set
(T,x) is Element of the carrier of T
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } ,T) is Element of the carrier of T
sup x is Element of the carrier of T
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V29( the carrier of x) V30( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
[: the carrier of x, the carrier of T:] is non empty set
bool [: the carrier of x, the carrier of T:] is non empty set
\\/ ( the mapping of x,T) is Element of the carrier of T
rng the mapping of x is Element of bool the carrier of T
"\/" ((rng the mapping of x),T) is Element of the carrier of T
rng e is Element of bool the carrier of T
"\/" ((rng e),T) is Element of the carrier of T
[x,("\/" (P,T))] is set
{x,("\/" (P,T))} is non empty finite countable set
{x} is non empty trivial finite V41(1) countable set
{{x,("\/" (P,T))},{x}} is non empty finite V38() countable set
f is Element of bool the carrier of T
f is Element of the carrier of x
X is Element of the carrier of x
x . X is Element of the carrier of T
the mapping of x . X is Element of the carrier of T
(id P) . X is set
P is Element of the carrier of T
e is Element of the carrier of T
(T,e) is non empty reflexive transitive antisymmetric strict directed NetStr over T
NetUniv T is non empty set
(T,(T,e)) is Element of the carrier of T
the carrier of (T,e) is non empty set
{ ("/\" ( { ((T,e) . b2) where b2 is Element of the carrier of (T,e) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,e) : verum } is set
"\/" ( { ("/\" ( { ((T,e) . b2) where b2 is Element of the carrier of (T,e) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,e) : verum } ,T) is Element of the carrier of T
[(T,e),P] is set
{(T,e),P} is non empty finite countable set
{(T,e)} is non empty trivial finite V41(1) countable set
{{(T,e),P},{(T,e)}} is non empty finite V38() countable set
x is Element of bool the carrier of T
P is Element of the carrier of T
x is non empty transitive directed NetStr over T
[x,P] is set
{x,P} is non empty finite countable set
{x} is non empty trivial finite V41(1) countable set
{{x,P},{x}} is non empty finite V38() countable set
NetUniv T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
f is non empty transitive strict directed NetStr over T
the carrier of f is non empty set
e is Element of the carrier of T
(T,x) is Element of the carrier of T
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } ,T) is Element of the carrier of T
{ (x . b1) where b1 is Element of the carrier of x : a1 <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : a1 <= b1 } ,T) is Element of the carrier of T
{ H1(b1) where b1 is Element of the carrier of x : S1[b1] } is set
X is Element of bool the carrier of T
X is non empty directed Element of bool the carrier of T
"\/" (X,T) is Element of the carrier of T
X /\ I is Element of bool the carrier of T
J is Element of the carrier of T
J is Element of the carrier of T
G is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : G <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : G <= b1 } ,T) is Element of the carrier of T
D is Element of the carrier of x
D9 is Element of the carrier of x
x . D9 is Element of the carrier of T
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V29( the carrier of x) V30( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]
[: the carrier of x, the carrier of T:] is non empty set
bool [: the carrier of x, the carrier of T:] is non empty set
the mapping of x . D9 is Element of the carrier of T
{ (x . b1) where b1 is Element of the carrier of x : D <= b1 } is set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
(T) is Relation-like Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
B is set
I is Element of bool the carrier of T
B is set
I is Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete TopRelStr
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
(T) is Relation-like Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
{ b1 where b1 is Element of bool the carrier of T : for b2 being Element of the carrier of T holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over T holds
( not [b3,b2] in (T) or b3 is_eventually_in b1 ) ) } is set
B is Element of bool the carrier of T
I is non empty directed Element of bool the carrier of T
"\/" (I,T) is Element of the carrier of T
id I is non empty Relation-like I -defined I -valued Function-like one-to-one V29(I) V30(I,I) Element of bool [:I,I:]
[:I,I:] is non empty set
bool [:I,I:] is non empty set
dom (id I) is Element of bool I
bool I is non empty set
rng (id I) is Element of bool I
[:I, the carrier of T:] is non empty set
bool [:I, the carrier of T:] is non empty set
P is non empty Relation-like I -defined the carrier of T -valued Function-like V29(I) V30(I, the carrier of T) Element of bool [:I, the carrier of T:]
(T,I,P) is non empty reflexive transitive strict monotone NetStr over T
e is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
NetUniv T is non empty set
(T,e) is Element of the carrier of T
the carrier of e is non empty set
{ ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,T)) where b1 is Element of the carrier of e : verum } is set
"\/" ( { ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,T)) where b1 is Element of the carrier of e : verum } ,T) is Element of the carrier of T
sup e is Element of the carrier of T
the mapping of e is non empty Relation-like the carrier of e -defined the carrier of T -valued Function-like V29( the carrier of e) V30( the carrier of e, the carrier of T) Element of bool [: the carrier of e, the carrier of T:]
[: the carrier of e, the carrier of T:] is non empty set
bool [: the carrier of e, the carrier of T:] is non empty set
\\/ ( the mapping of e,T) is Element of the carrier of T
rng the mapping of e is Element of bool the carrier of T
"\/" ((rng the mapping of e),T) is Element of the carrier of T
rng P is Element of bool the carrier of T
"\/" ((rng P),T) is Element of the carrier of T
[e,("\/" (I,T))] is set
{e,("\/" (I,T))} is non empty finite countable set
{e} is non empty trivial finite V41(1) countable set
{{e,("\/" (I,T))},{e}} is non empty finite V38() countable set
x is Element of bool the carrier of T
x is Element of the carrier of e
f is Element of the carrier of e
e . f is Element of the carrier of T
the mapping of e . f is Element of the carrier of T
(id I) . f is set
I is Element of the carrier of T
P is Element of the carrier of T
(T,P) is non empty reflexive transitive antisymmetric strict directed NetStr over T
NetUniv T is non empty set
(T,(T,P)) is Element of the carrier of T
the carrier of (T,P) is non empty set
{ ("/\" ( { ((T,P) . b2) where b2 is Element of the carrier of (T,P) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,P) : verum } is set
"\/" ( { ("/\" ( { ((T,P) . b2) where b2 is Element of the carrier of (T,P) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (T,P) : verum } ,T) is Element of the carrier of T
[(T,P),I] is set
{(T,P),I} is non empty finite countable set
{(T,P)} is non empty trivial finite V41(1) countable set
{{(T,P),I},{(T,P)}} is non empty finite V38() countable set
e is Element of bool the carrier of T
I is Element of the carrier of T
e is non empty transitive directed NetStr over T
[e,I] is set
{e,I} is non empty finite countable set
{e} is non empty trivial finite V41(1) countable set
{{e,I},{e}} is non empty finite V38() countable set
NetUniv T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
P is Element of the carrier of T
(T,e) is Element of the carrier of T
the carrier of e is non empty set
{ ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,T)) where b1 is Element of the carrier of e : verum } is set
"\/" ( { ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,T)) where b1 is Element of the carrier of e : verum } ,T) is Element of the carrier of T
{ (e . b1) where b1 is Element of the carrier of e : a1 <= b1 } is set
"/\" ( { (e . b1) where b1 is Element of the carrier of e : a1 <= b1 } ,T) is Element of the carrier of T
{ H1(b1) where b1 is Element of the carrier of e : S1[b1] } is set
f is Element of bool the carrier of T
X is non empty directed Element of bool the carrier of T
"\/" (X,T) is Element of the carrier of T
X /\ B is Element of bool the carrier of T
X is Element of the carrier of T
J is Element of the carrier of T
J is Element of the carrier of e
{ (e . b1) where b1 is Element of the carrier of e : J <= b1 } is set
"/\" ( { (e . b1) where b1 is Element of the carrier of e : J <= b1 } ,T) is Element of the carrier of T
G is Element of the carrier of e
D is Element of the carrier of e
e . D is Element of the carrier of T
the mapping of e is non empty Relation-like the carrier of e -defined the carrier of T -valued Function-like V29( the carrier of e) V30( the carrier of e, the carrier of T) Element of bool [: the carrier of e, the carrier of T:]
[: the carrier of e, the carrier of T:] is non empty set
bool [: the carrier of e, the carrier of T:] is non empty set
the mapping of e . D is Element of the carrier of T
{ (e . b1) where b1 is Element of the carrier of e : G <= b1 } is set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete TopRelStr
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
(T) is Relation-like Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
S is Element of bool the carrier of T
B is Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
(T) is Relation-like Convergence-Class of T
S is non empty transitive directed constant NetStr over T
NetUniv T is non empty set
the_value_of S is Element of the carrier of T
the carrier of T is non empty set
[S,(the_value_of S)] is set
{S,(the_value_of S)} is non empty finite countable set
{S} is non empty trivial finite V41(1) countable set
{{S,(the_value_of S)},{S}} is non empty finite V38() countable set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
B is non empty transitive strict directed NetStr over T
the carrier of B is non empty set
the_value_of B is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
(T) is Relation-like (CONSTANTS) Convergence-Class of T
B is non empty transitive directed NetStr over T
NetUniv T is non empty set
the carrier of T is non empty set
I is non empty transitive directed subnet of B
[:(NetUniv T), the carrier of T:] is non empty set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
P is non empty transitive strict directed NetStr over T
the carrier of P is non empty set
e is Element of the carrier of T
[B,e] is set
{B,e} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,e},{B}} is non empty finite V38() countable set
[I,e] is set
{I,e} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,e},{I}} is non empty finite V38() countable set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
the carrier of B is non empty set
{ (B . b1) where b1 is Element of the carrier of B : a1 <= b1 } is set
"/\" ( { (B . b1) where b1 is Element of the carrier of B : a1 <= b1 } ,T) is Element of the carrier of T
bool the carrier of T is non empty set
{ H1(b1) where b1 is Element of the carrier of B : S1[b1] } is set
the carrier of I is non empty set
{ (I . b1) where b1 is Element of the carrier of I : a1 <= b1 } is set
"/\" ( { (I . b1) where b1 is Element of the carrier of I : a1 <= b1 } ,T) is Element of the carrier of T
{ H2(b1) where b1 is Element of the carrier of I : S1[b1] } is set
(T,B) is Element of the carrier of T
{ ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } is set
"\/" ( { ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } ,T) is Element of the carrier of T
[: the carrier of I, the carrier of B:] is non empty set
bool [: the carrier of I, the carrier of B:] is non empty set
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
[: the carrier of I, the carrier of T:] is non empty set
bool [: the carrier of I, the carrier of T:] is non empty set
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
X is non empty Relation-like the carrier of I -defined the carrier of B -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of B) Element of bool [: the carrier of I, the carrier of B:]
the mapping of B * X is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
f is Element of bool the carrier of T
X is Element of bool the carrier of T
J is Element of the carrier of T
J is Element of the carrier of B
{ (B . b1) where b1 is Element of the carrier of B : J <= b1 } is set
"/\" ( { (B . b1) where b1 is Element of the carrier of B : J <= b1 } ,T) is Element of the carrier of T
G is Element of the carrier of B
D is Element of the carrier of I
{ (I . b1) where b1 is Element of the carrier of I : D <= b1 } is set
{ (B . b1) where b1 is Element of the carrier of B : G <= b1 } is set
"/\" ( { (I . b1) where b1 is Element of the carrier of I : D <= b1 } ,T) is Element of the carrier of T
x9 is Element of the carrier of T
X1 is set
X2 is Element of the carrier of I
I . X2 is Element of the carrier of T
the mapping of I . X2 is Element of the carrier of T
u is Element of the carrier of I
X . u is Element of the carrier of B
B . (X . u) is Element of the carrier of T
the mapping of B . (X . u) is Element of the carrier of T
"\/" (f,T) is Element of the carrier of T
"\/" (X,T) is Element of the carrier of T
(T,I) is Element of the carrier of T
{ ("/\" ( { (I . b2) where b2 is Element of the carrier of I : b1 <= b2 } ,T)) where b1 is Element of the carrier of I : verum } is set
"\/" ( { ("/\" ( { (I . b2) where b2 is Element of the carrier of I : b1 <= b2 } ,T)) where b1 is Element of the carrier of I : verum } ,T) is Element of the carrier of T
T is non empty 1-sorted
S is non empty transitive directed NetStr over T
B is set
S " B is transitive strict V271(T,S) SubNetStr of S
I is non empty transitive directed subnet of S
the carrier of I is non empty set
P is Element of the carrier of I
I . P is Element of the carrier of T
the carrier of T is non empty set
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
[: the carrier of I, the carrier of T:] is non empty set
bool [: the carrier of I, the carrier of T:] is non empty set
the mapping of I . P is Element of the carrier of T
the carrier of S is non empty set
the mapping of S is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S) V30( the carrier of S, the carrier of T) Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the mapping of S " B is Element of bool the carrier of S
bool the carrier of S is non empty set
the mapping of S . P is set
the mapping of S | the carrier of I is Relation-like the carrier of S -defined the carrier of T -valued Function-like Element of bool [: the carrier of S, the carrier of T:]
T is non empty reflexive RelStr
(T) is Relation-like Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
wayabove S is upper Element of bool the carrier of T
bool the carrier of T is non empty set
{ b1 where b1 is Element of the carrier of T : S is_way_below b1 } is set
I is non empty directed Element of bool the carrier of T
"\/" (I,T) is Element of the carrier of T
P is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete TopRelStr
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
(T) is Element of bool (bool the carrier of T)
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
TopStruct(# the carrier of (ConvergenceSpace (T)), the topology of (ConvergenceSpace (T)) #) is strict TopStruct
T is TopStruct
the carrier of T is set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
S is TopStruct
the carrier of S is set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
B is Element of bool (bool the carrier of S)
union B is Element of bool the carrier of S
I is Element of bool the carrier of S
P is Element of bool the carrier of S
I /\ P is Element of bool the carrier of S
T is non empty 1-sorted
the carrier of T is non empty set
S is non empty 1-sorted
the carrier of S is non empty set
B is non empty transitive strict directed NetStr over T
T is non empty 1-sorted
the carrier of T is non empty set
S is non empty 1-sorted
the carrier of S is non empty set
NetUniv T is non empty set
NetUniv S is non empty set
the_universe_of the carrier of S is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of S is V17() set
Tarski-Class (the_transitive-closure_of the carrier of S) is V17() subset-closed Tarski universal set
B is set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
I is non empty transitive strict directed NetStr over T
the carrier of I is non empty set
P is non empty transitive strict directed NetStr over S
the carrier of P is non empty set
I is non empty transitive strict directed NetStr over S
the carrier of I is non empty set
I is non empty transitive strict directed NetStr over S
the carrier of I is non empty set
P is non empty transitive strict directed NetStr over T
e is non empty transitive strict directed NetStr over T
the carrier of e is non empty set
e is non empty transitive strict directed NetStr over T
the carrier of e is non empty set
B is set
P is non empty transitive strict directed NetStr over S
I is set
the carrier of P is non empty set
T is non empty 1-sorted
S is non empty 1-sorted
B is set
I is non empty transitive directed NetStr over T
P is non empty transitive directed NetStr over S
the carrier of I is non empty set
e is Element of the carrier of I
the carrier of P is non empty set
x is Element of the carrier of P
f is Element of the carrier of P
P . f is Element of the carrier of S
the carrier of S is non empty set
the mapping of P is non empty Relation-like the carrier of P -defined the carrier of S -valued Function-like V29( the carrier of P) V30( the carrier of P, the carrier of S) Element of bool [: the carrier of P, the carrier of S:]
[: the carrier of P, the carrier of S:] is non empty set
bool [: the carrier of P, the carrier of S:] is non empty set
the mapping of P . f is Element of the carrier of S
X is Element of the carrier of I
I . X is Element of the carrier of T
the carrier of T is non empty set
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of T) Element of bool [: the carrier of I, the carrier of T:]
[: the carrier of I, the carrier of T:] is non empty set
bool [: the carrier of I, the carrier of T:] is non empty set
the mapping of I . X is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
B is non empty transitive directed NetStr over T
Lim B is Element of bool the carrier of T
I is non empty transitive directed NetStr over S
Lim I is Element of bool the carrier of S
P is Element of the carrier of T
e is Element of the carrier of S
x is a_neighborhood of e
Int x is open Element of bool the carrier of S
X is Element of bool the carrier of S
X is Element of bool the carrier of T
f is Element of bool the carrier of T
Int f is open Element of bool the carrier of T
J is a_neighborhood of P
the carrier of B is non empty set
J is Element of the carrier of B
the carrier of I is non empty set
G is Element of the carrier of I
D is Element of the carrier of I
I . D is Element of the carrier of S
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of S -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of S) Element of bool [: the carrier of I, the carrier of S:]
[: the carrier of I, the carrier of S:] is non empty set
bool [: the carrier of I, the carrier of S:] is non empty set
the mapping of I . D is Element of the carrier of S
D9 is Element of the carrier of B
B . D9 is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . D9 is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopStruct
Convergence T is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of T
Convergence S is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of S
NetUniv T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
NetUniv S is non empty set
[:(NetUniv S), the carrier of S:] is non empty set
B is set
I is set
[B,I] is set
{B,I} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,I},{B}} is non empty finite V38() countable set
P is Element of NetUniv T
e is Element of the carrier of T
[P,e] is Element of [:(NetUniv T), the carrier of T:]
{P,e} is non empty finite countable set
{P} is non empty trivial finite V41(1) countable set
{{P,e},{P}} is non empty finite V38() countable set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
f is non empty transitive strict directed NetStr over T
the carrier of f is non empty set
x is non empty transitive directed NetStr over T
Lim x is Element of bool the carrier of T
f is non empty transitive directed NetStr over S
X is Element of the carrier of S
Lim f is Element of bool the carrier of S
P is Element of NetUniv S
e is Element of the carrier of S
[P,e] is Element of [:(NetUniv S), the carrier of S:]
{P,e} is non empty finite countable set
{P} is non empty trivial finite V41(1) countable set
{{P,e},{P}} is non empty finite V38() countable set
the_universe_of the carrier of S is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of S is V17() set
Tarski-Class (the_transitive-closure_of the carrier of S) is V17() subset-closed Tarski universal set
f is non empty transitive strict directed NetStr over S
the carrier of f is non empty set
x is non empty transitive directed NetStr over S
Lim x is Element of bool the carrier of S
f is non empty transitive directed NetStr over T
X is Element of the carrier of T
Lim f is Element of bool the carrier of T
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of S
X is Element of the carrier of S
X is Element of the carrier of T
B is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of S
X is Element of the carrier of S
X is Element of the carrier of T
B is Element of the carrier of S
I is Element of the carrier of T
B is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of S
e is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of T
B is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of T
e is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is set
I is Element of the carrier of T
P is Element of the carrier of S
e is Element of the carrier of S
x is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is set
I is Element of the carrier of T
P is Element of the carrier of S
e is Element of the carrier of S
x is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is set
"\/" (B,T) is Element of the carrier of T
"\/" (B,S) is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of S
e is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is set
"/\" (B,T) is Element of the carrier of T
"/\" (B,S) is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of S
e is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
bool the carrier of T is non empty set
bool the carrier of S is non empty set
B is Element of bool the carrier of T
I is Element of bool the carrier of S
P is Element of the carrier of S
e is Element of the carrier of S
x is Element of the carrier of T
f is Element of the carrier of T
X is Element of the carrier of T
X is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of S
e is Element of the carrier of S
bool the carrier of S is non empty set
x is non empty directed Element of bool the carrier of S
"\/" (x,S) is Element of the carrier of S
bool the carrier of T is non empty set
f is non empty Element of bool the carrier of T
X is non empty directed Element of bool the carrier of T
"\/" (X,T) is Element of the carrier of T
X is Element of the carrier of T
J is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is non empty transitive directed NetStr over T
(T,B) is Element of the carrier of T
the carrier of B is non empty set
{ ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } is set
"\/" ( { ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } ,T) is Element of the carrier of T
I is non empty transitive directed NetStr over S
(S,I) is Element of the carrier of S
the carrier of I is non empty set
{ ("/\" ( { (I . b2) where b2 is Element of the carrier of I : b1 <= b2 } ,S)) where b1 is Element of the carrier of I : verum } is set
"\/" ( { ("/\" ( { (I . b2) where b2 is Element of the carrier of I : b1 <= b2 } ,S)) where b1 is Element of the carrier of I : verum } ,S) is Element of the carrier of S
x is set
f is Element of the carrier of B
{ (B . b1) where b1 is Element of the carrier of B : f <= b1 } is set
"/\" ( { (B . b1) where b1 is Element of the carrier of B : f <= b1 } ,T) is Element of the carrier of T
X is Element of the carrier of I
{ (I . b1) where b1 is Element of the carrier of I : X <= b1 } is set
J is set
G is Element of the carrier of B
B . G is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . G is Element of the carrier of T
D is Element of the carrier of I
I . D is Element of the carrier of S
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of S -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of S) Element of bool [: the carrier of I, the carrier of S:]
[: the carrier of I, the carrier of S:] is non empty set
bool [: the carrier of I, the carrier of S:] is non empty set
the mapping of I . D is Element of the carrier of S
J is set
G is Element of the carrier of I
I . G is Element of the carrier of S
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of S -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of S) Element of bool [: the carrier of I, the carrier of S:]
[: the carrier of I, the carrier of S:] is non empty set
bool [: the carrier of I, the carrier of S:] is non empty set
the mapping of I . G is Element of the carrier of S
D is Element of the carrier of B
B . D is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . D is Element of the carrier of T
"/\" ( { (I . b1) where b1 is Element of the carrier of I : X <= b1 } ,S) is Element of the carrier of S
x is set
f is Element of the carrier of I
{ (I . b1) where b1 is Element of the carrier of I : f <= b1 } is set
"/\" ( { (I . b1) where b1 is Element of the carrier of I : f <= b1 } ,S) is Element of the carrier of S
X is Element of the carrier of B
{ (B . b1) where b1 is Element of the carrier of B : X <= b1 } is set
J is set
G is Element of the carrier of I
I . G is Element of the carrier of S
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of S -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of S) Element of bool [: the carrier of I, the carrier of S:]
[: the carrier of I, the carrier of S:] is non empty set
bool [: the carrier of I, the carrier of S:] is non empty set
the mapping of I . G is Element of the carrier of S
D is Element of the carrier of B
B . D is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . D is Element of the carrier of T
J is set
G is Element of the carrier of B
B . G is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . G is Element of the carrier of T
D is Element of the carrier of I
I . D is Element of the carrier of S
the mapping of I is non empty Relation-like the carrier of I -defined the carrier of S -valued Function-like V29( the carrier of I) V30( the carrier of I, the carrier of S) Element of bool [: the carrier of I, the carrier of S:]
[: the carrier of I, the carrier of S:] is non empty set
bool [: the carrier of I, the carrier of S:] is non empty set
the mapping of I . D is Element of the carrier of S
"/\" ( { (B . b1) where b1 is Element of the carrier of B : X <= b1 } ,T) is Element of the carrier of T
T is non empty reflexive RelStr
S is non empty reflexive RelStr
I is non empty transitive directed NetStr over T
the carrier of I is non empty set
P is non empty transitive directed NetStr over S
the carrier of P is non empty set
e is non empty Relation-like the carrier of I -defined Function-like V29( the carrier of I) V115() V217() non-Empty net_set of the carrier of I,T
Iterated e is non empty transitive strict directed NetStr over T
x is non empty Relation-like the carrier of P -defined Function-like V29( the carrier of P) V115() V217() non-Empty net_set of the carrier of P,S
Iterated x is non empty transitive strict directed NetStr over S
the carrier of (Iterated e) is non empty set
the InternalRel of (Iterated e) is Relation-like the carrier of (Iterated e) -defined the carrier of (Iterated e) -valued Element of bool [: the carrier of (Iterated e), the carrier of (Iterated e):]
[: the carrier of (Iterated e), the carrier of (Iterated e):] is non empty set
bool [: the carrier of (Iterated e), the carrier of (Iterated e):] is non empty set
RelStr(# the carrier of (Iterated e), the InternalRel of (Iterated e) #) is strict RelStr
product e is non empty strict transitive directed RelStr
[:I,(product e):] is strict directed RelStr
the carrier of (Iterated x) is non empty set
the InternalRel of (Iterated x) is Relation-like the carrier of (Iterated x) -defined the carrier of (Iterated x) -valued Element of bool [: the carrier of (Iterated x), the carrier of (Iterated x):]
[: the carrier of (Iterated x), the carrier of (Iterated x):] is non empty set
bool [: the carrier of (Iterated x), the carrier of (Iterated x):] is non empty set
RelStr(# the carrier of (Iterated x), the InternalRel of (Iterated x) #) is strict RelStr
product x is non empty strict transitive directed RelStr
[:P,(product x):] is strict directed RelStr
the mapping of (Iterated e) is non empty Relation-like the carrier of (Iterated e) -defined the carrier of T -valued Function-like V29( the carrier of (Iterated e)) V30( the carrier of (Iterated e), the carrier of T) Element of bool [: the carrier of (Iterated e), the carrier of T:]
the carrier of T is non empty set
[: the carrier of (Iterated e), the carrier of T:] is non empty set
bool [: the carrier of (Iterated e), the carrier of T:] is non empty set
the mapping of (Iterated x) is non empty Relation-like the carrier of (Iterated x) -defined the carrier of S -valued Function-like V29( the carrier of (Iterated x)) V30( the carrier of (Iterated x), the carrier of S) Element of bool [: the carrier of (Iterated x), the carrier of S:]
the carrier of S is non empty set
[: the carrier of (Iterated x), the carrier of S:] is non empty set
bool [: the carrier of (Iterated x), the carrier of S:] is non empty set
dom the mapping of (Iterated e) is Element of bool the carrier of (Iterated e)
bool the carrier of (Iterated e) is non empty set
dom the mapping of (Iterated x) is Element of bool the carrier of (Iterated x)
bool the carrier of (Iterated x) is non empty set
X is set
the mapping of (Iterated e) . X is set
the mapping of (Iterated x) . X is set
the carrier of (product e) is non empty functional set
[: the carrier of I, the carrier of (product e):] is non empty set
J is Element of the carrier of I
J is Relation-like Function-like Element of the carrier of (product e)
[J,J] is Element of the carrier of [:I,(product e):]
the carrier of [:I,(product e):] is set
{J,J} is non empty finite countable set
{J} is non empty trivial finite V41(1) countable set
{{J,J},{J}} is non empty finite V38() countable set
the carrier of (product x) is non empty functional set
the mapping of (Iterated e) . (J,J) is set
[J,J] is set
the mapping of (Iterated e) . [J,J] is set
e . J is non empty RelStr
the carrier of (e . J) is non empty set
e . J is non empty transitive directed NetStr over T
the mapping of (e . J) is non empty Relation-like the carrier of (e . J) -defined the carrier of T -valued Function-like V29( the carrier of (e . J)) V30( the carrier of (e . J), the carrier of T) Element of bool [: the carrier of (e . J), the carrier of T:]
the carrier of (e . J) is non empty set
[: the carrier of (e . J), the carrier of T:] is non empty set
bool [: the carrier of (e . J), the carrier of T:] is non empty set
J . J is Element of the carrier of (e . J)
the mapping of (e . J) . (J . J) is Element of the carrier of T
G is Element of the carrier of P
x . G is non empty RelStr
the carrier of (x . G) is non empty set
x . G is non empty transitive directed NetStr over S
the mapping of (x . G) is non empty Relation-like the carrier of (x . G) -defined the carrier of S -valued Function-like V29( the carrier of (x . G)) V30( the carrier of (x . G), the carrier of S) Element of bool [: the carrier of (x . G), the carrier of S:]
the carrier of (x . G) is non empty set
[: the carrier of (x . G), the carrier of S:] is non empty set
bool [: the carrier of (x . G), the carrier of S:] is non empty set
D is Relation-like Function-like Element of the carrier of (product x)
D . G is Element of the carrier of (x . G)
the mapping of (x . G) . (D . G) is Element of the carrier of S
the mapping of (Iterated x) . (G,D) is set
[G,D] is set
{G,D} is non empty finite countable set
{G} is non empty trivial finite V41(1) countable set
{{G,D},{G}} is non empty finite V38() countable set
the mapping of (Iterated x) . [G,D] is set
T is non empty reflexive RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
I is non empty transitive directed NetStr over T
the carrier of I is non empty set
P is non empty transitive directed NetStr over S
the carrier of P is non empty set
e is non empty Relation-like the carrier of I -defined Function-like V29( the carrier of I) V115() V217() non-Empty net_set of the carrier of I,T
x is non empty Relation-like the carrier of P -defined Function-like V29( the carrier of P) set
rng x is set
f is set
X is non empty transitive directed NetStr over T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
(S) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of S
NetUniv T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
B is set
I is Element of NetUniv T
P is Element of the carrier of T
[I,P] is Element of [:(NetUniv T), the carrier of T:]
{I,P} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,P},{I}} is non empty finite V38() countable set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
f is non empty transitive strict directed NetStr over T
the carrier of f is non empty set
e is non empty transitive strict directed NetStr over S
NetUniv S is non empty set
x is non empty transitive strict directed NetStr over T
(T,x) is Element of the carrier of T
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,T)) where b1 is Element of the carrier of x : verum } ,T) is Element of the carrier of T
(S,e) is Element of the carrier of S
the carrier of e is non empty set
{ ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,S)) where b1 is Element of the carrier of e : verum } is set
"\/" ( { ("/\" ( { (e . b2) where b2 is Element of the carrier of e : b1 <= b2 } ,S)) where b1 is Element of the carrier of e : verum } ,S) is Element of the carrier of S
f is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
(S) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
(T) is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
(S) is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
(S) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of S
ConvergenceSpace (S) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (S)) is Element of bool (bool the carrier of (ConvergenceSpace (S)))
the carrier of (ConvergenceSpace (S)) is non empty set
bool the carrier of (ConvergenceSpace (S)) is non empty set
bool (bool the carrier of (ConvergenceSpace (S))) is non empty set
{ b1 where b1 is Element of bool the carrier of T : for b2 being Element of the carrier of T holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over T holds
( not [b3,b2] in (T) or b3 is_eventually_in b1 ) ) } is set
{ b1 where b1 is Element of bool the carrier of S : for b2 being Element of the carrier of S holds
( not b2 in b1 or for b3 being non empty transitive directed NetStr over S holds
( not [b3,b2] in (S) or b3 is_eventually_in b1 ) ) } is set
P is set
e is Element of bool the carrier of T
x is Element of bool the carrier of S
f is Element of the carrier of S
X is non empty transitive directed NetStr over S
[X,f] is set
{X,f} is non empty finite countable set
{X} is non empty trivial finite V41(1) countable set
{{X,f},{X}} is non empty finite V38() countable set
J is non empty transitive directed NetStr over T
X is Element of the carrier of T
[J,X] is set
{J,X} is non empty finite countable set
{J} is non empty trivial finite V41(1) countable set
{{J,X},{J}} is non empty finite V38() countable set
P is set
e is Element of bool the carrier of S
x is Element of bool the carrier of T
f is Element of the carrier of T
X is non empty transitive directed NetStr over T
[X,f] is set
{X,f} is non empty finite countable set
{X} is non empty trivial finite V41(1) countable set
{{X,f},{X}} is non empty finite V38() countable set
J is non empty transitive directed NetStr over S
X is Element of the carrier of S
[J,X] is set
{J,X} is non empty finite countable set
{J} is non empty trivial finite V41(1) countable set
{{J,X},{J}} is non empty finite V38() countable set
T is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is set
I is Element of the carrier of T
P is Element of the carrier of S
e is Element of the carrier of S
x is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
B is Element of the carrier of S
waybelow B is non empty directed lower Element of bool the carrier of S
bool the carrier of S is non empty set
{ b1 where b1 is Element of the carrier of S : b1 is_way_below B } is set
I is Element of the carrier of S
waybelow I is non empty directed lower Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : b1 is_way_below I } is set
B is Element of the carrier of T
waybelow B is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{ b1 where b1 is Element of the carrier of T : b1 is_way_below B } is set
I is Element of the carrier of T
waybelow I is non empty directed lower Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : b1 is_way_below I } is set
B is Element of the carrier of S
I is Element of the carrier of S
P is Element of the carrier of T
e is Element of the carrier of T
x is Element of the carrier of T
f is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
the carrier of T is non empty set
B is non empty transitive directed NetStr over T
NetUniv T is non empty set
I is Element of the carrier of T
[B,I] is set
{B,I} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,I},{B}} is non empty finite V38() countable set
P is Element of the carrier of T
waybelow P is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{ b1 where b1 is Element of the carrier of T : b1 is_way_below P } is set
e is Element of the carrier of T
waybelow e is non empty directed lower Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : b1 is_way_below e } is set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
e is non empty transitive strict directed NetStr over T
the carrier of e is non empty set
(T,B) is Element of the carrier of T
the carrier of B is non empty set
{ ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } is set
"\/" ( { ("/\" ( { (B . b2) where b2 is Element of the carrier of B : b1 <= b2 } ,T)) where b1 is Element of the carrier of B : verum } ,T) is Element of the carrier of T
P is Element of the carrier of T
x is Element of the carrier of T
{ b1 where b1 is Element of the carrier of T : not x <= b1 } is set
X is Element of the carrier of B
{ (B . b1) where b1 is Element of the carrier of B : X <= b1 } is set
"/\" ( { (B . b1) where b1 is Element of the carrier of B : X <= b1 } ,T) is Element of the carrier of T
J is Element of the carrier of T
G is Element of the carrier of B
B . G is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . G is Element of the carrier of T
B " { b1 where b1 is Element of the carrier of T : not x <= b1 } is transitive strict V271(T,B) SubNetStr of B
X is non empty transitive directed subnet of B
X is V17() subset-closed Tarski universal set
the carrier of (B " { b1 where b1 is Element of the carrier of T : not x <= b1 } ) is set
the carrier of X is non empty set
J is non empty transitive strict directed NetStr over T
the carrier of J is non empty set
J is non empty transitive directed subnet of X
[J,I] is set
{J,I} is non empty finite countable set
{J} is non empty trivial finite V41(1) countable set
{{J,I},{J}} is non empty finite V38() countable set
[:(NetUniv T), the carrier of T:] is non empty set
J is non empty transitive strict directed NetStr over T
the carrier of J is non empty set
the carrier of J is non empty set
{ (J . b1) where b1 is Element of the carrier of J : a1 <= b1 } is set
"/\" ( { (J . b1) where b1 is Element of the carrier of J : a1 <= b1 } ,T) is Element of the carrier of T
{ H1(b1) where b1 is Element of the carrier of J : S1[b1] } is set
bool the carrier of T is non empty set
D is Element of bool the carrier of T
(T,J) is Element of the carrier of T
{ ("/\" ( { (J . b2) where b2 is Element of the carrier of J : b1 <= b2 } ,T)) where b1 is Element of the carrier of J : verum } is set
"\/" ( { ("/\" ( { (J . b2) where b2 is Element of the carrier of J : b1 <= b2 } ,T)) where b1 is Element of the carrier of J : verum } ,T) is Element of the carrier of T
D9 is non empty directed Element of bool the carrier of T
E9 is Element of the carrier of T
x9 is Element of the carrier of J
{ (J . b1) where b1 is Element of the carrier of J : x9 <= b1 } is set
"/\" ( { (J . b1) where b1 is Element of the carrier of J : x9 <= b1 } ,T) is Element of the carrier of T
X1 is Element of the carrier of J
X2 is Element of the carrier of J
[: the carrier of J, the carrier of X:] is non empty set
bool [: the carrier of J, the carrier of X:] is non empty set
the mapping of J is non empty Relation-like the carrier of J -defined the carrier of T -valued Function-like V29( the carrier of J) V30( the carrier of J, the carrier of T) Element of bool [: the carrier of J, the carrier of T:]
[: the carrier of J, the carrier of T:] is non empty set
bool [: the carrier of J, the carrier of T:] is non empty set
the mapping of X is non empty Relation-like the carrier of X -defined the carrier of T -valued Function-like V29( the carrier of X) V30( the carrier of X, the carrier of T) Element of bool [: the carrier of X, the carrier of T:]
[: the carrier of X, the carrier of T:] is non empty set
bool [: the carrier of X, the carrier of T:] is non empty set
u is non empty Relation-like the carrier of J -defined the carrier of X -valued Function-like V29( the carrier of J) V30( the carrier of J, the carrier of X) Element of bool [: the carrier of J, the carrier of X:]
the mapping of X * u is non empty Relation-like the carrier of J -defined the carrier of T -valued Function-like V29( the carrier of J) V30( the carrier of J, the carrier of T) Element of bool [: the carrier of J, the carrier of T:]
J . X2 is Element of the carrier of T
the mapping of J . X2 is Element of the carrier of T
u . X2 is Element of the carrier of X
X . (u . X2) is Element of the carrier of T
the mapping of X . (u . X2) is Element of the carrier of T
j is Element of the carrier of T
the carrier of T is non empty set
B is non empty transitive directed NetStr over T
the carrier of B is non empty set
I is Element of the carrier of T
[B,I] is set
{B,I} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,I},{B}} is non empty finite V38() countable set
P is non empty Relation-like the carrier of B -defined Function-like V29( the carrier of B) V115() V217() non-Empty net_set of the carrier of B,T
Iterated P is non empty transitive strict directed NetStr over T
[(Iterated P),I] is set
{(Iterated P),I} is non empty finite countable set
{(Iterated P)} is non empty trivial finite V41(1) countable set
{{(Iterated P),I},{(Iterated P)}} is non empty finite V38() countable set
NetUniv T is non empty set
[:(NetUniv T), the carrier of T:] is non empty set
e is Element of the carrier of B
P . e is non empty transitive directed NetStr over T
B . e is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . e is Element of the carrier of T
[(P . e),(B . e)] is set
{(P . e),(B . e)} is non empty finite countable set
{(P . e)} is non empty trivial finite V41(1) countable set
{{(P . e),(B . e)},{(P . e)}} is non empty finite V38() countable set
(T,(Iterated P)) is Element of the carrier of T
the carrier of (Iterated P) is non empty set
{ ("/\" ( { ((Iterated P) . b2) where b2 is Element of the carrier of (Iterated P) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (Iterated P) : verum } is set
"\/" ( { ("/\" ( { ((Iterated P) . b2) where b2 is Element of the carrier of (Iterated P) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (Iterated P) : verum } ,T) is Element of the carrier of T
e is Element of the carrier of T
waybelow e is non empty directed lower Element of bool the carrier of T
bool the carrier of T is non empty set
{ b1 where b1 is Element of the carrier of T : b1 is_way_below e } is set
f is Element of the carrier of T
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
(T) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (T)) is Element of bool (bool the carrier of (ConvergenceSpace (T)))
the carrier of (ConvergenceSpace (T)) is non empty set
bool the carrier of (ConvergenceSpace (T)) is non empty set
bool (bool the carrier of (ConvergenceSpace (T))) is non empty set
TopRelStr(# the carrier of T, the InternalRel of T,(T) #) is non empty strict TopRelStr
the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #) is non empty set
the InternalRel of TopRelStr(# the carrier of T, the InternalRel of T,(T) #) is Relation-like the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #) -defined the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #) -valued Element of bool [: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #):]
[: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #):] is non empty set
bool [: the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #), the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #):] is non empty set
RelStr(# the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(T) #), the InternalRel of TopRelStr(# the carrier of T, the InternalRel of T,(T) #) #) is strict RelStr
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
X is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr
J is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete TopRelStr
J is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous TopRelStr
the topology of J is Element of bool (bool the carrier of J)
the carrier of J is non empty set
bool the carrier of J is non empty set
bool (bool the carrier of J) is non empty set
(J) is Element of bool (bool the carrier of J)
(J) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of J
ConvergenceSpace (J) is non empty strict TopSpace-like TopStruct
the topology of (ConvergenceSpace (J)) is Element of bool (bool the carrier of (ConvergenceSpace (J)))
the carrier of (ConvergenceSpace (J)) is non empty set
bool the carrier of (ConvergenceSpace (J)) is non empty set
bool (bool the carrier of (ConvergenceSpace (J))) is non empty set
G is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
D is non empty transitive directed NetStr over G
the carrier of D is non empty set
the carrier of G is non empty set
D9 is non empty Relation-like the carrier of D -defined Function-like V29( the carrier of D) V115() V217() non-Empty net_set of the carrier of D,G
Iterated D9 is non empty transitive strict directed NetStr over G
Convergence G is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of G
Convergence (ConvergenceSpace (T)) is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of ConvergenceSpace (T)
E9 is Element of the carrier of G
X1 is Element of the carrier of G
x9 is Element of the carrier of G
(G,(Iterated D9)) is Element of the carrier of G
the carrier of (Iterated D9) is non empty set
{ ("/\" ( { ((Iterated D9) . b2) where b2 is Element of the carrier of (Iterated D9) : b1 <= b2 } ,G)) where b1 is Element of the carrier of (Iterated D9) : verum } is set
"\/" ( { ("/\" ( { ((Iterated D9) . b2) where b2 is Element of the carrier of (Iterated D9) : b1 <= b2 } ,G)) where b1 is Element of the carrier of (Iterated D9) : verum } ,G) is Element of the carrier of G
j is Element of the carrier of D
D9 . j is non empty transitive directed NetStr over G
D . j is Element of the carrier of G
the mapping of D is non empty Relation-like the carrier of D -defined the carrier of G -valued Function-like V29( the carrier of D) V30( the carrier of D, the carrier of G) Element of bool [: the carrier of D, the carrier of G:]
[: the carrier of D, the carrier of G:] is non empty set
bool [: the carrier of D, the carrier of G:] is non empty set
the mapping of D . j is Element of the carrier of G
[(D9 . j),(D . j)] is set
{(D9 . j),(D . j)} is non empty finite countable set
{(D9 . j)} is non empty trivial finite V41(1) countable set
{{(D9 . j),(D . j)},{(D9 . j)}} is non empty finite V38() countable set
e is Element of the carrier of B
P . e is non empty transitive directed NetStr over T
B . e is Element of the carrier of T
the mapping of B is non empty Relation-like the carrier of B -defined the carrier of T -valued Function-like V29( the carrier of B) V30( the carrier of B, the carrier of T) Element of bool [: the carrier of B, the carrier of T:]
[: the carrier of B, the carrier of T:] is non empty set
bool [: the carrier of B, the carrier of T:] is non empty set
the mapping of B . e is Element of the carrier of T
[(P . e),(B . e)] is set
{(P . e),(B . e)} is non empty finite countable set
{(P . e)} is non empty trivial finite V41(1) countable set
{{(P . e),(B . e)},{(P . e)}} is non empty finite V38() countable set
[(Iterated D9),X1] is set
{(Iterated D9),X1} is non empty finite countable set
{(Iterated D9)} is non empty trivial finite V41(1) countable set
{{(Iterated D9),X1},{(Iterated D9)}} is non empty finite V38() countable set
Lim (Iterated D9) is Element of bool the carrier of G
bool the carrier of G is non empty set
wayabove E9 is upper Element of bool the carrier of G
{ b1 where b1 is Element of the carrier of G : E9 is_way_below b1 } is set
uparrow E9 is non empty filtered upper Element of bool the carrier of G
{E9} is non empty trivial finite V41(1) countable Element of bool the carrier of G
uparrow {E9} is non empty upper Element of bool the carrier of G
"\/" ((waybelow e),T) is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
NetUniv T is non empty set
S is Element of the carrier of T
B is non empty transitive directed NetStr over T
Lim B is Element of bool the carrier of T
bool the carrier of T is non empty set
(T) is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of T
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
Convergence (ConvergenceSpace (T)) is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of ConvergenceSpace (T)
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
I is non empty transitive strict directed NetStr over T
the carrier of I is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
Convergence T is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of T
[B,S] is set
{B,S} is non empty finite countable set
{B} is non empty trivial finite V41(1) countable set
{{B,S},{B}} is non empty finite V38() countable set
[I,S] is set
{I,S} is non empty finite countable set
{I} is non empty trivial finite V41(1) countable set
{{I,S},{I}} is non empty finite V38() countable set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete RelStr
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
B is non empty set
the carrier of T is non empty set
the_universe_of the carrier of T is non empty V17() subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is V17() set
Tarski-Class (the_transitive-closure_of the carrier of T) is V17() subset-closed Tarski universal set
I is non empty Relation-like non-empty non empty-yielding B -defined Function-like V29(B) set
K203(B, the carrier of T) is non empty Relation-like non-empty non empty-yielding B -defined { the carrier of T} -valued Function-like constant V29(B) V30(B,{ the carrier of T}) Element of bool [:B,{ the carrier of T}:]
{ the carrier of T} is non empty trivial finite V41(1) countable set
[:B,{ the carrier of T}:] is non empty set
bool [:B,{ the carrier of T}:] is non empty set
P is non empty Relation-like non-empty non empty-yielding B -defined Function-like V29(B) V99() V100() ManySortedFunction of I,K203(B, the carrier of T)
\// (P,T) is Relation-like dom P -defined the carrier of T -valued Function-like V29( dom P) V30( dom P, the carrier of T) Element of bool [:(dom P), the carrier of T:]
dom P is set
[:(dom P), the carrier of T:] is set
bool [:(dom P), the carrier of T:] is non empty set
//\ ((\// (P,T)),T) is Element of the carrier of T
Frege P is non empty Relation-like non-empty non empty-yielding product (doms P) -defined Function-like V29( product (doms P)) V99() V100() ManySortedFunction of K203((product (doms P)),B),K203((product (doms P)), the carrier of T)
doms P is Relation-like non-empty Function-like set
product (doms P) is non empty functional with_common_domain product-like set
K203((product (doms P)),B) is non empty Relation-like non-empty non empty-yielding product (doms P) -defined {B} -valued Function-like constant V29( product (doms P)) V30( product (doms P),{B}) Element of bool [:(product (doms P)),{B}:]
{B} is non empty trivial finite V41(1) countable set
[:(product (doms P)),{B}:] is non empty set
bool [:(product (doms P)),{B}:] is non empty set
K203((product (doms P)), the carrier of T) is non empty Relation-like non-empty non empty-yielding product (doms P) -defined { the carrier of T} -valued Function-like constant V29( product (doms P)) V30( product (doms P),{ the carrier of T}) Element of bool [:(product (doms P)),{ the carrier of T}:]
[:(product (doms P)),{ the carrier of T}:] is non empty set
bool [:(product (doms P)),{ the carrier of T}:] is non empty set
/\\ ((Frege P),T) is Relation-like dom (Frege P) -defined the carrier of T -valued Function-like V29( dom (Frege P)) V30( dom (Frege P), the carrier of T) Element of bool [:(dom (Frege P)), the carrier of T:]
dom (Frege P) is set
[:(dom (Frege P)), the carrier of T:] is set
bool [:(dom (Frege P)), the carrier of T:] is non empty set
\\/ ((/\\ ((Frege P),T)),T) is Element of the carrier of T
[:B,B:] is non empty set
bool [:B,B:] is non empty set
dom P is Element of bool B
bool B is non empty set
[:B, the carrier of T:] is non empty set
bool [:B, the carrier of T:] is non empty set
x is Relation-like B -defined B -valued Element of bool [:B,B:]
f is non empty Relation-like B -defined the carrier of T -valued Function-like V29(B) V30(B, the carrier of T) Element of bool [:B, the carrier of T:]
NetStr(# B,x,f #) is non empty strict NetStr over T
the carrier of NetStr(# B,x,f #) is non empty set
X is Element of the carrier of NetStr(# B,x,f #)
J is Element of the carrier of NetStr(# B,x,f #)
[X,J] is Element of the carrier of [:NetStr(# B,x,f #),NetStr(# B,x,f #):]
[:NetStr(# B,x,f #),NetStr(# B,x,f #):] is strict RelStr
the carrier of [:NetStr(# B,x,f #),NetStr(# B,x,f #):] is set
{X,J} is non empty finite countable set
{X} is non empty trivial finite V41(1) countable set
{{X,J},{X}} is non empty finite V38() countable set
the InternalRel of NetStr(# B,x,f #) is Relation-like the carrier of NetStr(# B,x,f #) -defined the carrier of NetStr(# B,x,f #) -valued Element of bool [: the carrier of NetStr(# B,x,f #), the carrier of NetStr(# B,x,f #):]
[: the carrier of NetStr(# B,x,f #), the carrier of NetStr(# B,x,f #):] is non empty set
bool [: the carrier of NetStr(# B,x,f #), the carrier of NetStr(# B,x,f #):] is non empty set
X is Element of the carrier of NetStr(# B,x,f #)
J is Element of the carrier of NetStr(# B,x,f #)
J is Element of the carrier of NetStr(# B,x,f #)
X is Element of the carrier of NetStr(# B,x,f #)
J is Element of the carrier of NetStr(# B,x,f #)
J is non empty Relation-like B -defined Function-like V29(B) set
X is non empty transitive strict directed NetStr over T
the carrier of X is non empty set
J is set
J . J is set
bool the carrier of T is non empty set
G is Element of B
P . G is non empty Relation-like I . G -defined the carrier of T -valued Function-like V29(I . G) V30(I . G, the carrier of T) Element of bool [:(I . G), the carrier of T:]
I . G is non empty set
[:(I . G), the carrier of T:] is non empty set
bool [:(I . G), the carrier of T:] is non empty set
rng (P . G) is non empty Element of bool the carrier of T
D is Element of bool the carrier of T
J . G is set
(T,(I . G),(P . G)) is non empty reflexive transitive strict monotone NetStr over T
J is non empty Relation-like the carrier of X -defined Function-like V29( the carrier of X) V115() V217() non-Empty net_set of the carrier of X,T
G is set
J . G is set
I . G is set
D is Element of B
I . D is non empty set
P . D is non empty Relation-like I . D -defined the carrier of T -valued Function-like V29(I . D) V30(I . D, the carrier of T) Element of bool [:(I . D), the carrier of T:]
[:(I . D), the carrier of T:] is non empty set
bool [:(I . D), the carrier of T:] is non empty set
(T,(I . D),(P . D)) is non empty reflexive transitive strict monotone NetStr over T
D9 is non empty reflexive transitive strict monotone NetStr over T
the carrier of D9 is non empty set
Carrier J is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V29( the carrier of X) set
dom (Frege P) is functional with_common_domain Element of bool (product (doms P))
bool (product (doms P)) is non empty set
dom (/\\ ((Frege P),T)) is Element of bool (dom (Frege P))
bool (dom (Frege P)) is non empty set
NetUniv T is non empty set
G is Element of the carrier of X
J . G is non empty transitive directed NetStr over T
D is Element of B
I . D is non empty set
P . D is non empty Relation-like I . D -defined the carrier of T -valued Function-like V29(I . D) V30(I . D, the carrier of T) Element of bool [:(I . D), the carrier of T:]
[:(I . D), the carrier of T:] is non empty set
bool [:(I . D), the carrier of T:] is non empty set
(T,(I . D),(P . D)) is non empty reflexive transitive strict monotone NetStr over T
D9 is non empty transitive strict directed NetStr over T
the carrier of D9 is non empty set
G is Element of the carrier of X
J . G is non empty transitive directed NetStr over T
X . G is Element of the carrier of T
the mapping of X is non empty Relation-like the carrier of X -defined the carrier of T -valued Function-like V29( the carrier of X) V30( the carrier of X, the carrier of T) Element of bool [: the carrier of X, the carrier of T:]
[: the carrier of X, the carrier of T:] is non empty set
bool [: the carrier of X, the carrier of T:] is non empty set
the mapping of X . G is Element of the carrier of T
[(J . G),(X . G)] is set
{(J . G),(X . G)} is non empty finite countable set
{(J . G)} is non empty trivial finite V41(1) countable set
{{(J . G),(X . G)},{(J . G)}} is non empty finite V38() countable set
D is Element of B
I . D is non empty set
P . D is non empty Relation-like I . D -defined the carrier of T -valued Function-like V29(I . D) V30(I . D, the carrier of T) Element of bool [:(I . D), the carrier of T:]
[:(I . D), the carrier of T:] is non empty set
bool [:(I . D), the carrier of T:] is non empty set
(T,(I . D),(P . D)) is non empty reflexive transitive strict monotone NetStr over T
\\/ ((P . D),T) is Element of the carrier of T
D9 is non empty reflexive transitive directed monotone eventually-directed NetStr over T
the mapping of D9 is non empty Relation-like the carrier of D9 -defined the carrier of T -valued Function-like V29( the carrier of D9) V30( the carrier of D9, the carrier of T) Element of bool [: the carrier of D9, the carrier of T:]
the carrier of D9 is non empty set
[: the carrier of D9, the carrier of T:] is non empty set
bool [: the carrier of D9, the carrier of T:] is non empty set
\\/ ( the mapping of D9,T) is Element of the carrier of T
sup D9 is Element of the carrier of T
(T,D9) is Element of the carrier of T
{ ("/\" ( { (D9 . b2) where b2 is Element of the carrier of D9 : b1 <= b2 } ,T)) where b1 is Element of the carrier of D9 : verum } is set
"\/" ( { ("/\" ( { (D9 . b2) where b2 is Element of the carrier of D9 : b1 <= b2 } ,T)) where b1 is Element of the carrier of D9 : verum } ,T) is Element of the carrier of T
Iterated J is non empty transitive strict directed NetStr over T
the carrier of (Iterated J) is non empty set
{ ((Iterated J) . b1) where b1 is Element of the carrier of (Iterated J) : a1 <= b1 } is set
product (Carrier J) is non empty functional with_common_domain product-like set
[: the carrier of X,(product (Carrier J)):] is non empty set
[: the carrier of X,(product (doms P)):] is non empty set
[:[: the carrier of X,(product (doms P)):], the carrier of T:] is non empty set
bool [:[: the carrier of X,(product (doms P)):], the carrier of T:] is non empty set
the mapping of (Iterated J) is non empty Relation-like the carrier of (Iterated J) -defined the carrier of T -valued Function-like V29( the carrier of (Iterated J)) V30( the carrier of (Iterated J), the carrier of T) Element of bool [: the carrier of (Iterated J), the carrier of T:]
[: the carrier of (Iterated J), the carrier of T:] is non empty set
bool [: the carrier of (Iterated J), the carrier of T:] is non empty set
G is non empty Relation-like [: the carrier of X,(product (doms P)):] -defined the carrier of T -valued Function-like V29([: the carrier of X,(product (doms P)):]) V30([: the carrier of X,(product (doms P)):], the carrier of T) Element of bool [:[: the carrier of X,(product (doms P)):], the carrier of T:]
{ (G . (b1,a2)) where b1 is Element of the carrier of X : a1 <= b1 } is set
{ ("/\" (H2(b1),T)) where b1 is Element of the carrier of (Iterated J) : verum } is set
{ H5(b1,b2) where b1 is Element of the carrier of X, b2 is Relation-like Function-like doms P -compatible Element of product (doms P) : S1[b2] } is set
{ H4(b1) where b1 is Relation-like Function-like doms P -compatible Element of product (doms P) : S1[b1] } is set
x9 is Element of the carrier of X
X1 is Relation-like Function-like doms P -compatible Element of product (doms P)
(Frege P) . X1 is non empty Relation-like B -defined the carrier of T -valued Function-like V29(B) V30(B, the carrier of T) Element of bool [:B, the carrier of T:]
rng ((Frege P) . X1) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"/\" ((rng ((Frege P) . X1)),T) is Element of the carrier of T
{ (G . (b1,X1)) where b1 is Element of the carrier of X : x9 <= b1 } is set
"/\" (H3(x9,X1),T) is Element of the carrier of T
dom ((Frege P) . X1) is Element of bool B
X2 is set
product J is non empty strict transitive directed RelStr
the carrier of (product J) is non empty functional set
u is Element of the carrier of X
G . (u,X1) is Element of the carrier of T
[u,X1] is set
{u,X1} is non empty finite countable set
{u} is non empty trivial finite V41(1) countable set
{{u,X1},{u}} is non empty finite V38() countable set
G . [u,X1] is set
j is set
u is Element of B
e is set
((Frege P) . X1) . e is set
P . u is non empty Relation-like I . u -defined the carrier of T -valued Function-like V29(I . u) V30(I . u, the carrier of T) Element of bool [:(I . u), the carrier of T:]
I . u is non empty set
[:(I . u), the carrier of T:] is non empty set
bool [:(I . u), the carrier of T:] is non empty set
X1 . u is set
(P . u) . (X1 . u) is set
(T,(I . u),(P . u)) is non empty reflexive transitive strict monotone NetStr over T
the mapping of (T,(I . u),(P . u)) is non empty Relation-like the carrier of (T,(I . u),(P . u)) -defined the carrier of T -valued Function-like V29( the carrier of (T,(I . u),(P . u))) V30( the carrier of (T,(I . u),(P . u)), the carrier of T) Element of bool [: the carrier of (T,(I . u),(P . u)), the carrier of T:]
the carrier of (T,(I . u),(P . u)) is non empty set
[: the carrier of (T,(I . u),(P . u)), the carrier of T:] is non empty set
bool [: the carrier of (T,(I . u),(P . u)), the carrier of T:] is non empty set
the mapping of (T,(I . u),(P . u)) . (X1 . u) is set
J . u is non empty transitive directed NetStr over T
the mapping of (J . u) is non empty Relation-like the carrier of (J . u) -defined the carrier of T -valued Function-like V29( the carrier of (J . u)) V30( the carrier of (J . u), the carrier of T) Element of bool [: the carrier of (J . u), the carrier of T:]
the carrier of (J . u) is non empty set
[: the carrier of (J . u), the carrier of T:] is non empty set
bool [: the carrier of (J . u), the carrier of T:] is non empty set
the mapping of (J . u) . (X1 . u) is set
u is set
((Frege P) . X1) . u is set
j is Element of B
e is Element of the carrier of X
P . u is Relation-like Function-like set
X1 . u is set
(P . u) . (X1 . u) is set
I . j is non empty set
P . j is non empty Relation-like I . j -defined the carrier of T -valued Function-like V29(I . j) V30(I . j, the carrier of T) Element of bool [:(I . j), the carrier of T:]
[:(I . j), the carrier of T:] is non empty set
bool [:(I . j), the carrier of T:] is non empty set
(T,(I . j),(P . j)) is non empty reflexive transitive strict monotone NetStr over T
the mapping of (T,(I . j),(P . j)) is non empty Relation-like the carrier of (T,(I . j),(P . j)) -defined the carrier of T -valued Function-like V29( the carrier of (T,(I . j),(P . j))) V30( the carrier of (T,(I . j),(P . j)), the carrier of T) Element of bool [: the carrier of (T,(I . j),(P . j)), the carrier of T:]
the carrier of (T,(I . j),(P . j)) is non empty set
[: the carrier of (T,(I . j),(P . j)), the carrier of T:] is non empty set
bool [: the carrier of (T,(I . j),(P . j)), the carrier of T:] is non empty set
X1 . e is set
the mapping of (T,(I . j),(P . j)) . (X1 . e) is set
J . e is non empty transitive directed NetStr over T
the mapping of (J . e) is non empty Relation-like the carrier of (J . e) -defined the carrier of T -valued Function-like V29( the carrier of (J . e)) V30( the carrier of (J . e), the carrier of T) Element of bool [: the carrier of (J . e), the carrier of T:]
the carrier of (J . e) is non empty set
[: the carrier of (J . e), the carrier of T:] is non empty set
bool [: the carrier of (J . e), the carrier of T:] is non empty set
the mapping of (J . e) . (X1 . e) is set
G . (e,X1) is Element of the carrier of T
[e,X1] is set
{e,X1} is non empty finite countable set
{e} is non empty trivial finite V41(1) countable set
{{e,X1},{e}} is non empty finite V38() countable set
G . [e,X1] is set
x9 is Element of the carrier of (Iterated J)
{ ((Iterated J) . b1) where b1 is Element of the carrier of (Iterated J) : x9 <= b1 } is set
"/\" (H2(x9),T) is Element of the carrier of T
X1 is Element of the carrier of X
X2 is Relation-like Function-like doms P -compatible Element of product (doms P)
[X1,X2] is Element of [: the carrier of X,(product (doms P)):]
{X1,X2} is non empty finite countable set
{X1} is non empty trivial finite V41(1) countable set
{{X1,X2},{X1}} is non empty finite V38() countable set
{ (G . (b1,X2)) where b1 is Element of the carrier of X : X1 <= b1 } is set
"/\" (H3(X1,X2),T) is Element of the carrier of T
the InternalRel of (Iterated J) is Relation-like the carrier of (Iterated J) -defined the carrier of (Iterated J) -valued Element of bool [: the carrier of (Iterated J), the carrier of (Iterated J):]
[: the carrier of (Iterated J), the carrier of (Iterated J):] is non empty set
bool [: the carrier of (Iterated J), the carrier of (Iterated J):] is non empty set
RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) is strict RelStr
product J is non empty strict transitive directed RelStr
[:X,(product J):] is strict directed RelStr
the carrier of [:X,(product J):] is set
the InternalRel of [:X,(product J):] is Relation-like the carrier of [:X,(product J):] -defined the carrier of [:X,(product J):] -valued Element of bool [: the carrier of [:X,(product J):], the carrier of [:X,(product J):]:]
[: the carrier of [:X,(product J):], the carrier of [:X,(product J):]:] is set
bool [: the carrier of [:X,(product J):], the carrier of [:X,(product J):]:] is non empty set
RelStr(# the carrier of [:X,(product J):], the InternalRel of [:X,(product J):] #) is strict RelStr
the carrier of (product J) is non empty functional set
u is Relation-like Function-like Element of the carrier of (product J)
e is set
J . e is set
u . e is set
u is Element of the carrier of X
i is Element of B
I . i is non empty set
P . i is non empty Relation-like I . i -defined the carrier of T -valued Function-like V29(I . i) V30(I . i, the carrier of T) Element of bool [:(I . i), the carrier of T:]
[:(I . i), the carrier of T:] is non empty set
bool [:(I . i), the carrier of T:] is non empty set
(T,(I . i),(P . i)) is non empty reflexive transitive strict monotone NetStr over T
u . u is Element of the carrier of (J . u)
J . u is non empty RelStr
the carrier of (J . u) is non empty set
the carrier of (T,(I . i),(P . i)) is non empty set
k is Element of the carrier of (T,(I . i),(P . i))
e is set
u is Element of the carrier of X
the mapping of (Iterated J) . (u,X2) is set
[u,X2] is set
{u,X2} is non empty finite countable set
{u} is non empty trivial finite V41(1) countable set
{{u,X2},{u}} is non empty finite V38() countable set
the mapping of (Iterated J) . [u,X2] is set
[u,X2] is Element of [: the carrier of X,(product (doms P)):]
j is Element of the carrier of X
[j,u] is Element of the carrier of [:X,(product J):]
{j,u} is non empty finite countable set
{j} is non empty trivial finite V41(1) countable set
{{j,u},{j}} is non empty finite V38() countable set
i is Element of the carrier of X
[i,u] is Element of the carrier of [:X,(product J):]
{i,u} is non empty finite countable set
{i} is non empty trivial finite V41(1) countable set
{{i,u},{i}} is non empty finite V38() countable set
u is Element of the carrier of (Iterated J)
(Iterated J) . u is Element of the carrier of T
the mapping of (Iterated J) . u is Element of the carrier of T
{ H6(b1) where b1 is Element of the carrier of X : S2[b1] } is set
bool the carrier of T is non empty set
{ H7(b1) where b1 is Element of the carrier of (Iterated J) : S3[b1] } is set
e is Element of bool the carrier of T
u is Element of bool the carrier of T
i is Element of the carrier of T
u is Element of the carrier of (Iterated J)
(Iterated J) . u is Element of the carrier of T
the mapping of (Iterated J) . u is Element of the carrier of T
k is Element of the carrier of X
f is non empty Relation-like the carrier of X -defined Function-like Carrier J -compatible V29( the carrier of X) Element of product (Carrier J)
[k,f] is Element of [: the carrier of X,(product (Carrier J)):]
{k,f} is non empty finite countable set
{k} is non empty trivial finite V41(1) countable set
{{k,f},{k}} is non empty finite V38() countable set
the mapping of (Iterated J) . (k,X2) is set
[k,X2] is set
{k,X2} is non empty finite countable set
{{k,X2},{k}} is non empty finite V38() countable set
the mapping of (Iterated J) . [k,X2] is set
G . (k,X2) is Element of the carrier of T
G . [k,X2] is set
a is Element of the carrier of T
j is Element of the carrier of X
[j,u] is Element of the carrier of [:X,(product J):]
{j,u} is non empty finite countable set
{j} is non empty trivial finite V41(1) countable set
{{j,u},{j}} is non empty finite V38() countable set
k9 is Element of the carrier of X
f9 is Relation-like Function-like Element of the carrier of (product J)
[k9,f9] is Element of the carrier of [:X,(product J):]
{k9,f9} is non empty finite countable set
{k9} is non empty trivial finite V41(1) countable set
{{k9,f9},{k9}} is non empty finite V38() countable set
k9 is Element of B
I . k9 is non empty set
P . k9 is non empty Relation-like I . k9 -defined the carrier of T -valued Function-like V29(I . k9) V30(I . k9, the carrier of T) Element of bool [:(I . k9), the carrier of T:]
[:(I . k9), the carrier of T:] is non empty set
bool [:(I . k9), the carrier of T:] is non empty set
(T,(I . k9),(P . k9)) is non empty reflexive transitive strict monotone NetStr over T
J . k is non empty transitive directed NetStr over T
the carrier of (T,(I . k9),(P . k9)) is non empty set
u . k is Element of the carrier of (J . k)
J . k is non empty RelStr
the carrier of (J . k) is non empty set
f9 . k is Element of the carrier of (J . k)
f9k is Element of the carrier of (T,(I . k9),(P . k9))
(T,(I . k9),(P . k9)) . f9k is Element of the carrier of T
the mapping of (T,(I . k9),(P . k9)) is non empty Relation-like the carrier of (T,(I . k9),(P . k9)) -defined the carrier of T -valued Function-like V29( the carrier of (T,(I . k9),(P . k9))) V30( the carrier of (T,(I . k9),(P . k9)), the carrier of T) Element of bool [: the carrier of (T,(I . k9),(P . k9)), the carrier of T:]
[: the carrier of (T,(I . k9),(P . k9)), the carrier of T:] is non empty set
bool [: the carrier of (T,(I . k9),(P . k9)), the carrier of T:] is non empty set
the mapping of (T,(I . k9),(P . k9)) . f9k is Element of the carrier of T
[k,X2] is Element of [: the carrier of X,(product (doms P)):]
kg is Element of the carrier of (Iterated J)
(Iterated J) . kg is Element of the carrier of T
the mapping of (Iterated J) . kg is Element of the carrier of T
g9k is Element of the carrier of (T,(I . k9),(P . k9))
(T,(I . k9),(P . k9)) . g9k is Element of the carrier of T
the mapping of (T,(I . k9),(P . k9)) . g9k is Element of the carrier of T
x9 is set
X1 is Element of the carrier of (Iterated J)
{ ((Iterated J) . b1) where b1 is Element of the carrier of (Iterated J) : X1 <= b1 } is set
"/\" (H2(X1),T) is Element of the carrier of T
X2 is Element of the carrier of X
u is Relation-like Function-like doms P -compatible Element of product (doms P)
[X2,u] is Element of [: the carrier of X,(product (doms P)):]
{X2,u} is non empty finite countable set
{X2} is non empty trivial finite V41(1) countable set
{{X2,u},{X2}} is non empty finite V38() countable set
{ (G . (b1,u)) where b1 is Element of the carrier of X : X2 <= b1 } is set
"/\" (H3(X2,u),T) is Element of the carrier of T
x9 is set
X1 is Element of the carrier of X
X2 is Relation-like Function-like doms P -compatible Element of product (doms P)
{ (G . (b1,X2)) where b1 is Element of the carrier of X : X1 <= b1 } is set
"/\" (H3(X1,X2),T) is Element of the carrier of T
[X1,X2] is Element of [: the carrier of X,(product (doms P)):]
{X1,X2} is non empty finite countable set
{X1} is non empty trivial finite V41(1) countable set
{{X1,X2},{X1}} is non empty finite V38() countable set
u is Element of the carrier of (Iterated J)
{ ((Iterated J) . b1) where b1 is Element of the carrier of (Iterated J) : u <= b1 } is set
"/\" (H2(u),T) is Element of the carrier of T
x9 is set
X1 is Relation-like Function-like doms P -compatible Element of product (doms P)
(Frege P) . X1 is non empty Relation-like B -defined the carrier of T -valued Function-like V29(B) V30(B, the carrier of T) Element of bool [:B, the carrier of T:]
rng ((Frege P) . X1) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"/\" ((rng ((Frege P) . X1)),T) is Element of the carrier of T
(/\\ ((Frege P),T)) . X1 is set
//\ (((Frege P) . X1),T) is Element of the carrier of T
X1 is set
(/\\ ((Frege P),T)) . X1 is set
X2 is Relation-like Function-like doms P -compatible Element of product (doms P)
(Frege P) . X2 is non empty Relation-like B -defined the carrier of T -valued Function-like V29(B) V30(B, the carrier of T) Element of bool [:B, the carrier of T:]
//\ (((Frege P) . X2),T) is Element of the carrier of T
rng ((Frege P) . X2) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"/\" ((rng ((Frege P) . X2)),T) is Element of the carrier of T
rng (/\\ ((Frege P),T)) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
(T,(Iterated J)) is Element of the carrier of T
{ ("/\" ( { ((Iterated J) . b2) where b2 is Element of the carrier of (Iterated J) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (Iterated J) : verum } is set
"\/" ( { ("/\" ( { ((Iterated J) . b2) where b2 is Element of the carrier of (Iterated J) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (Iterated J) : verum } ,T) is Element of the carrier of T
{ (//\ ((\// (P,T)),T)) where b1 is Element of the carrier of X : verum } is set
{ ("/\" ( { (X . b2) where b2 is Element of the carrier of X : b1 <= b2 } ,T)) where b1 is Element of the carrier of X : verum } is set
u is Element of the carrier of X
{ (X . b1) where b1 is Element of the carrier of X : u <= b1 } is set
"/\" ( { (X . b1) where b1 is Element of the carrier of X : u <= b1 } ,T) is Element of the carrier of T
dom (\// (P,T)) is Element of bool (dom P)
bool (dom P) is non empty set
e is set
u is Element of the carrier of X
X . u is Element of the carrier of T
the mapping of X is non empty Relation-like the carrier of X -defined the carrier of T -valued Function-like V29( the carrier of X) V30( the carrier of X, the carrier of T) Element of bool [: the carrier of X, the carrier of T:]
[: the carrier of X, the carrier of T:] is non empty set
bool [: the carrier of X, the carrier of T:] is non empty set
the mapping of X . u is Element of the carrier of T
i is set
u is set
(\// (P,T)) . u is set
u is set
(\// (P,T)) . u is set
i is Element of the carrier of X
X . i is Element of the carrier of T
the mapping of X . i is Element of the carrier of T
rng (\// (P,T)) is non empty Element of bool the carrier of T
u is set
j is Element of the carrier of X
{ (X . b1) where b1 is Element of the carrier of X : j <= b1 } is set
"/\" ( { (X . b1) where b1 is Element of the carrier of X : j <= b1 } ,T) is Element of the carrier of T
u is set
the Element of the carrier of X is Element of the carrier of X
{ (X . b1) where b1 is Element of the carrier of X : the Element of the carrier of X <= b1 } is set
"/\" ( { (X . b1) where b1 is Element of the carrier of X : the Element of the carrier of X <= b1 } ,T) is Element of the carrier of T
u is set
{(//\ ((\// (P,T)),T))} is non empty trivial finite V41(1) countable Element of bool the carrier of T
"\/" ( { ("/\" ( { (X . b2) where b2 is Element of the carrier of X : b1 <= b2 } ,T)) where b1 is Element of the carrier of X : verum } ,T) is Element of the carrier of T
x9 is Element of the carrier of T
{x9} is non empty trivial finite V41(1) countable Element of bool the carrier of T
"\/" ({x9},T) is Element of the carrier of T
(T,X) is Element of the carrier of T
[X,(//\ ((\// (P,T)),T))] is set
{X,(//\ ((\// (P,T)),T))} is non empty finite countable set
{X} is non empty trivial finite V41(1) countable set
{{X,(//\ ((\// (P,T)),T))},{X}} is non empty finite V38() countable set
[(Iterated J),(//\ ((\// (P,T)),T))] is set
{(Iterated J),(//\ ((\// (P,T)),T))} is non empty finite countable set
{(Iterated J)} is non empty trivial finite V41(1) countable set
{{(Iterated J),(//\ ((\// (P,T)),T))},{(Iterated J)}} is non empty finite V38() countable set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
Convergence T is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of T
(T) is Relation-like (CONSTANTS) (SUBNETS) Convergence-Class of T
the carrier of T is non empty set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
ConvergenceSpace (T) is non empty strict TopSpace-like TopStruct
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
(S) is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of S
ConvergenceSpace (S) is non empty strict TopSpace-like TopStruct
Convergence (ConvergenceSpace (S)) is Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) topological Convergence-Class of ConvergenceSpace (S)
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is upper Element of bool the carrier of T
B is non empty directed Element of bool the carrier of T
"\/" (B,T) is Element of the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is upper Element of bool the carrier of T
B is Element of the carrier of T
uparrow B is Element of bool the carrier of T
{B} is non empty trivial finite V41(1) countable Element of bool the carrier of T
uparrow {B} is Element of bool the carrier of T
I is set
P is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of the carrier of T
B is Element of bool the carrier of T
waybelow S is non empty directed lower (T) Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : b1 is_way_below S } is set
"\/" ((waybelow S),T) is Element of the carrier of T
(waybelow S) /\ B is Element of bool the carrier of T
I is Element of the carrier of T
P is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
S is Element of the carrier of T
{ (wayabove b1) where b1 is Element of the carrier of T : b1 is_way_below S } is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
I is set
P is Element of the carrier of T
wayabove P is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : P is_way_below b1 } is set
I is Element of bool (bool the carrier of T)
P is Element of bool the carrier of T
e is Element of the carrier of T
wayabove e is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : e is_way_below b1 } is set
P is set
e is Element of the carrier of T
wayabove e is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : e is_way_below b1 } is set
Intersect I is Element of bool the carrier of T
P is Element of bool the carrier of T
e is Element of the carrier of T
wayabove e is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : e is_way_below b1 } is set
x is upper Element of bool the carrier of T
uparrow e is non empty filtered upper Element of bool the carrier of T
{e} is non empty trivial finite V41(1) countable Element of bool the carrier of T
uparrow {e} is non empty upper Element of bool the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
{ (wayabove b1) where b1 is Element of the carrier of T : verum } is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of T is Element of bool (bool the carrier of T)
B is set
I is Element of the carrier of T
wayabove I is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : I is_way_below b1 } is set
B is Element of bool (bool the carrier of T)
I is Element of the carrier of T
P is Element of the carrier of T
{ (wayabove b1) where b1 is Element of the carrier of T : b1 is_way_below P } is set
e is I -quasi_basis open Element of bool (bool the carrier of T)
x is set
f is Element of the carrier of T
wayabove f is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : f is_way_below b1 } is set
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is upper Element of bool the carrier of T
B is Element of the carrier of T
I is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
S is Element of the carrier of T
uparrow S is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{S} is non empty trivial finite V41(1) countable Element of bool the carrier of T
uparrow {S} is non empty upper Element of bool the carrier of T
Int (uparrow S) is open Element of bool the carrier of T
wayabove S is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : S is_way_below b1 } is set
B is set
I is Element of the carrier of T
P is Element of bool the carrier of T
e is Element of the carrier of T
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V186() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous () TopRelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
S is Element of bool the carrier of T
Int S is open Element of bool the carrier of T
{ (wayabove b1) where b1 is Element of the carrier of T : wayabove b1 c= S } is set
union { (wayabove b1) where b1 is Element of the carrier of T : wayabove b1 c= S } is set
{ (wayabove b1) where b1 is Element of the carrier of T : verum } is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in { (wayabove b1) where b2 is Element of the carrier of T : verum } & b1 c= S ) } is set
e is set
x is Element of bool the carrier of T
f is Element of the carrier of T
wayabove f is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : f is_way_below b1 } is set
e is set
x is Element of the carrier of T
wayabove x is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : x is_way_below b1 } is set
bool (bool the carrier of T) is non empty set