:: 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({{}})

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

F

F

{ F

{ F

B is set

the Element of F

P is Element of F

F

F

B is set

I is Element of F

P is Element of F

F

F

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

{ b

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

{ b

[#] 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 . b

"\/" ( { ("/\" ( { (S . b

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

"\/" ( { ("/\" ( { (S . b

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

"/\" ( { (S . b

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

"\/" ( { ("/\" ( { (S . b

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

"/\" ( { (S . b

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

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) . b

(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 . b

"\/" ( { ("/\" ( { (S . b

sup S is Element of the carrier of T

{ (S . b

"/\" ( { (S . b

{ H

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

"/\" ( { (S . b

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

{ H

\\/ ( 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 . b

"\/" ( { ("/\" ( { (S . b

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

"/\" ( { (S . b

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

P is Element of the carrier of T

{ (S . b

"/\" ( { (S . b

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

"\/" ( { ("/\" ( { (S . b

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) . b

"\/" ( { ("/\" ( { ((T,S) . b

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) . b

"/\" ( { ((T,S) . b

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) . b

"/\" ( { ((T,S) . b

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

B is Element of bool the carrier of T

the Element of the carrier of S is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

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

"/\" ( { (S . b

f is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

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

{ (S . b

{ (S . b

"/\" ( { (S . b

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

{ b

( not b

( not [b

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

"\/" ( { ("/\" ( { (x . b

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) . b

"\/" ( { ("/\" ( { ((T,e) . b

[(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 . b

"\/" ( { ("/\" ( { (x . b

{ (x . b

"/\" ( { (x . b

{ H

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

"/\" ( { (x . b

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

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

{ b

( not b

( not [b

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

"\/" ( { ("/\" ( { (e . b

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) . b

"\/" ( { ("/\" ( { ((T,P) . b

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