:: WAYBEL11 semantic presentation

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()
is set
bool 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

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

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

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

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()
is non empty trivial finite V38() V41(1) countable Element of bool K219()
is non empty finite countable set
bool 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
is non empty trivial finite V38() V41(1) countable set
is non empty finite V38() countable set

bool [:K219(),K219():] is non empty non trivial non finite set

RelStr(# ,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

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 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
() ` is Element of bool the carrier of T
the carrier of T \ () 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

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

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

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

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

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

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

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

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

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
() ` is upper Element of bool the carrier of T
the carrier of T \ () is set

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
() ` is upper Element of bool the carrier of T
the carrier of T \ () is set
B is upper Element of bool the carrier of T
Int (() `) is open Element of 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
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
() ` is upper Element of bool the carrier of T
the carrier of T \ () is set
P is Element of bool the carrier of T
e is 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 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

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
[:(), the carrier of T:] is non empty set
bool [:(), the carrier of T:] is non empty set
S is Relation-like NetUniv T -defined the carrier of T -valued Element of bool [:(), the carrier 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

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
[:(), 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

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

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

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

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

I is non empty transitive strict directed NetStr over T
the carrier of I is non empty set

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,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

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

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

[:{S},{S}:] is non empty finite countable set
bool [:{S},{S}:] is non empty finite V38() countable set

bool {S} is non empty finite V38() countable set

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

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

[:{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

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 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

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

the topology of () is Element of bool (bool the carrier of ())
the carrier of () is non empty set
bool the carrier of () is non empty set
bool (bool the carrier of ()) 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

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
[:(), 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

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

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

the topology of () is Element of bool (bool the carrier of ())
the carrier of () is non empty set
bool the carrier of () is non empty set
bool (bool the carrier of ()) 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

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

{ 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

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
[:(), 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

x is non empty transitive strict directed NetStr over T
the carr