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 carr