:: YELLOW_6 semantic presentation

K273() is non empty epsilon-transitive epsilon-connected ordinal V48() cardinal limit_cardinal countable denumerable Element of bool K269()
K269() is set
bool K269() is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V48() cardinal limit_cardinal countable denumerable set
bool omega is non empty V48() set
bool K273() is non empty V48() set
K318() is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V48() cardinal {} -element Cardinal-yielding countable Function-yielding V136() set
{{}} is functional non empty trivial 1 -element with_common_domain set
1 is non empty set
K296({{}}) is M22({{}})
[:K296({{}}),{{}}:] is Relation-like set
bool [:K296({{}}),{{}}:] is non empty set
K36(K296({{}}),{{}}) is functional non empty set
T is set
the_transitive-closure_of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of T) is non empty epsilon-transitive subset-closed Tarski universal set
T is set
(T) is set
the_transitive-closure_of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of T) is non empty epsilon-transitive subset-closed Tarski universal set
T is set
(T) is epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of T) is non empty epsilon-transitive subset-closed Tarski universal set
T is non empty epsilon-transitive subset-closed Tarski universal set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
product C is functional with_common_domain product-like set
card (proj1 C) is epsilon-transitive epsilon-connected ordinal cardinal set
card T is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (proj2 C) is epsilon-transitive epsilon-connected ordinal cardinal set
union (proj2 C) is set
Union C is set
Funcs ((proj1 C),(Union C)) is functional set
T is non empty set
C is Relation-like T -defined Function-like non empty V14(T) 1-sorted-yielding set
Carrier C is Relation-like T -defined Function-like non empty V14(T) set
CC is Element of T
(Carrier C) . CC is set
C . CC is 1-sorted
the carrier of (C . CC) is set
CCC is 1-sorted
the carrier of CCC is set
the 1-sorted is 1-sorted
{ the 1-sorted } is non empty trivial 1 -element set
[:{{}},{ the 1-sorted }:] is Relation-like non empty set
bool [:{{}},{ the 1-sorted }:] is non empty set
{{}} --> the 1-sorted is Relation-like {{}} -defined { the 1-sorted } -valued Function-like constant non empty V14({{}}) quasi_total Element of bool [:{{}},{ the 1-sorted }:]
C is Relation-like {{}} -defined { the 1-sorted } -valued Function-like constant non empty V14({{}}) quasi_total Element of bool [:{{}},{ the 1-sorted }:]
CC is set
proj1 C is non empty set
C . CC is set
dom C is functional non empty trivial 1 -element with_common_domain Element of bool {{}}
bool {{}} is non empty set
T is Relation-like Function-like 1-sorted-yielding set
proj2 T is set
C is set
proj1 T is set
CC is set
T . CC is set
C is 1-sorted
T is set
C is 1-sorted
T --> C is Relation-like T -defined {C} -valued Function-like constant V14(T) quasi_total Element of bool [:T,{C}:]
{C} is non empty trivial 1 -element set
[:T,{C}:] is Relation-like set
bool [:T,{C}:] is non empty set
CC is set
proj1 (T --> C) is set
(T --> C) . CC is set
dom (T --> C) is Element of bool T
bool T is non empty set
rng (T --> C) is trivial Element of bool {C}
bool {C} is non empty set
T is set
the non empty 1-sorted is non empty 1-sorted
T --> the non empty 1-sorted is Relation-like T -defined { the non empty 1-sorted } -valued Function-like constant V14(T) quasi_total 1-sorted-yielding Element of bool [:T,{ the non empty 1-sorted }:]
{ the non empty 1-sorted } is non empty trivial 1 -element set
[:T,{ the non empty 1-sorted }:] is Relation-like set
bool [:T,{ the non empty 1-sorted }:] is non empty set
CC is set
proj2 (T --> the non empty 1-sorted ) is trivial set
rng (T --> the non empty 1-sorted ) is trivial Element of bool { the non empty 1-sorted }
bool { the non empty 1-sorted } is non empty set
T is non empty set
C is Relation-like T -defined Function-like non empty V14(T) 1-sorted-yielding RelStr-yielding set
product C is strict RelStr
the carrier of (product C) is set
Carrier C is Relation-like T -defined Function-like non empty V14(T) set
product (Carrier C) is functional with_common_domain product-like set
T is set
C is Relation-like T -defined Function-like V14(T) 1-sorted-yielding non-Empty set
Carrier C is Relation-like T -defined Function-like V14(T) set
proj2 (Carrier C) is set
dom (Carrier C) is Element of bool T
bool T is non empty set
CC is set
(Carrier C) . CC is set
C . CC is set
CCC is 1-sorted
the carrier of CCC is set
dom C is Element of bool T
proj2 C is set
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
C is lower Element of bool the carrier of T
C ` is Element of bool the carrier of T
the carrier of T \ C is set
CC is Element of the carrier of T
CCC 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
C is upper Element of bool the carrier of T
C ` is Element of bool the carrier of T
the carrier of T \ C is set
CC is Element of the carrier of T
CCC is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
[#] T is non empty non proper lower upper Element of bool the carrier of T
bool the carrier of T is non empty set
C is Element of the carrier of T
CC is Element of the carrier of T
CCC is Element of the carrier of T
C is Element of the carrier of T
CC is Element of the carrier of T
CCC is Element of the carrier of T
T is set
BoolePoset T is non empty strict V97() reflexive transitive antisymmetric V124() V125() V126() V154() V155() V156() up-complete /\-complete non void RelStr
K222(T) is non empty V104() V111() V118() V127() L10()
K224(K222(T)) is non empty strict V97() reflexive transitive antisymmetric V124() V125() V126() V154() V155() V156() up-complete /\-complete non void RelStr
the carrier of (BoolePoset T) is non empty set
C is Element of the carrier of (BoolePoset T)
CC is Element of the carrier of (BoolePoset T)
C "\/" CC is Element of the carrier of (BoolePoset T)
C \/ CC is set
BoolePoset {} is non empty strict V97() reflexive transitive antisymmetric V124() V125() V126() V154() V155() V156() directed up-complete /\-complete non void RelStr
K222({}) is non empty V104() V111() V118() V127() L10()
K224(K222({})) is non empty strict V97() reflexive transitive antisymmetric V124() V125() V126() V154() V155() V156() up-complete /\-complete non void RelStr
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
the carrier of RelStr(# the carrier of T, the InternalRel of T #) is non empty set
C is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
CC is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
CCC is Element of the carrier of T
C9 is Element of the carrier of T
x is Element of the carrier of T
y is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
[C,y] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
[:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty strict RelStr
the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
{C,y} is non empty set
{C} is non empty trivial 1 -element set
{{C,y},{C}} is non empty set
[CC,y] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
{CC,y} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,y},{CC}} is non empty set
C is Element of the carrier of T
CC is Element of the carrier of T
the carrier of RelStr(# the carrier of T, the InternalRel of T #) is non empty set
CCC is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
C9 is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
x is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
y is Element of the carrier of T
[CCC,x] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
[:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty strict RelStr
the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
{CCC,x} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,x},{CCC}} is non empty set
the InternalRel of RelStr(# the carrier of T, the InternalRel of T #) is Relation-like the carrier of RelStr(# the carrier of T, the InternalRel of T #) -defined the carrier of RelStr(# the carrier of T, the InternalRel of T #) -valued Element of bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):]
[: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is Relation-like non empty set
bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
[C9,x] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
{C9,x} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,x},{C9}} is non empty set
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
the carrier of RelStr(# the carrier of T, the InternalRel of T #) is non empty set
C is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
CC is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
CCC is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
[CC,CCC] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
[:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty strict RelStr
the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
{CC,CCC} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,CCC},{CC}} is non empty set
the InternalRel of RelStr(# the carrier of T, the InternalRel of T #) is Relation-like the carrier of RelStr(# the carrier of T, the InternalRel of T #) -defined the carrier of RelStr(# the carrier of T, the InternalRel of T #) -valued Element of bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):]
[: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is Relation-like non empty set
bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
x is Element of the carrier of T
y is Element of the carrier of T
[C,CC] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
{C,CC} is non empty set
{C} is non empty trivial 1 -element set
{{C,CC},{C}} is non empty set
C9 is Element of the carrier of T
[C9,y] is V15() Element of the carrier of [:T,T:]
[:T,T:] is non empty strict RelStr
the carrier of [:T,T:] is non empty set
{C9,y} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,y},{C9}} is non empty set
C is Element of the carrier of T
CC is Element of the carrier of T
CCC is Element of the carrier of T
the carrier of RelStr(# the carrier of T, the InternalRel of T #) is non empty set
x is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
y is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
[x,y] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
[:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty strict RelStr
the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
{x,y} is non empty set
{x} is non empty trivial 1 -element set
{{x,y},{x}} is non empty set
the InternalRel of RelStr(# the carrier of T, the InternalRel of T #) is Relation-like the carrier of RelStr(# the carrier of T, the InternalRel of T #) -defined the carrier of RelStr(# the carrier of T, the InternalRel of T #) -valued Element of bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):]
[: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is Relation-like non empty set
bool [: the carrier of RelStr(# the carrier of T, the InternalRel of T #), the carrier of RelStr(# the carrier of T, the InternalRel of T #):] is non empty set
C9 is Element of the carrier of RelStr(# the carrier of T, the InternalRel of T #)
[C9,x] is V15() Element of the carrier of [:RelStr(# the carrier of T, the InternalRel of T #),RelStr(# the carrier of T, the InternalRel of T #):]
{C9,x} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,x},{C9}} is non empty set
[C,CCC] is V15() Element of the carrier of [:T,T:]
[:T,T:] is non empty strict RelStr
the carrier of [:T,T:] is non empty set
{C,CCC} is non empty set
{C} is non empty trivial 1 -element set
{{C,CCC},{C}} is non empty set
T is non empty set
C is non empty RelStr
the carrier of C is non empty set
[:T, the carrier of C:] is Relation-like non empty set
bool [:T, the carrier of C:] is non empty set
CC is Relation-like T -defined the carrier of C -valued Function-like non empty V14(T) quasi_total Element of bool [:T, the carrier of C:]
CCC is Element of T
CC . CCC is set
CC . CCC is Element of the carrier of C
T is set
the non empty RelStr is non empty RelStr
T --> the non empty RelStr is Relation-like T -defined { the non empty RelStr } -valued Function-like constant V14(T) quasi_total 1-sorted-yielding RelStr-yielding Element of bool [:T,{ the non empty RelStr }:]
{ the non empty RelStr } is non empty trivial 1 -element set
[:T,{ the non empty RelStr }:] is Relation-like set
bool [:T,{ the non empty RelStr }:] is non empty set
CC is set
proj2 (T --> the non empty RelStr ) is trivial set
rng (T --> the non empty RelStr ) is trivial Element of bool { the non empty RelStr }
bool { the non empty RelStr } is non empty set
T is non empty set
C is Relation-like T -defined Function-like non empty V14(T) 1-sorted-yielding RelStr-yielding non-Empty set
product C is non empty strict RelStr
T is directed RelStr
C is directed RelStr
[:T,C:] is strict RelStr
the carrier of C is set
bool the carrier of C is non empty set
[#] C is non proper Element of bool the carrier of C
the carrier of T is set
bool the carrier of T is non empty set
[#] T is non proper Element of bool the carrier of T
CCC is directed Element of bool the carrier of T
CC is directed Element of bool the carrier of C
[:CCC,CC:] is Relation-like directed Element of bool the carrier of [:T,C:]
the carrier of [:T,C:] is set
bool the carrier of [:T,C:] is non empty set
[#] [:T,C:] is non proper Element of bool the carrier of [:T,C:]
T is RelStr
the carrier of T is set
T ~ is strict RelStr
the carrier of (T ~) 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 Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
T is RelStr
the carrier of T is set
C is RelStr
the carrier of C 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 Relation-like 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 C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
RelStr(# the carrier of C, the InternalRel of C #) is strict RelStr
CC is Element of the carrier of T
CCC is Element of the carrier of T
C9 is Element of the carrier of C
x is Element of the carrier of C
[C9,x] is V15() set
{C9,x} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,x},{C9}} is non empty set
T is 1-sorted
C is non empty 1-sorted
the carrier of C is non empty set
T is RelStr
the carrier of T 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 Relation-like 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
CC is Element of the carrier of C
[: the carrier of T, the carrier of C:] is Relation-like set
bool [: the carrier of T, the carrier of C:] is non empty set
the carrier of T --> CC is Relation-like the carrier of T -defined the carrier of C -valued Function-like constant V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of C:]
CCC is Relation-like the carrier of T -defined the carrier of C -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of C:]
NetStr(# the carrier of T, the InternalRel of T,CCC #) is strict NetStr over C
the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) is set
the InternalRel of NetStr(# the carrier of T, the InternalRel of T,CCC #) is Relation-like the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) -defined the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) -valued Element of bool [: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #):]
[: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #):] is Relation-like set
bool [: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #):] is non empty set
RelStr(# the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the InternalRel of NetStr(# the carrier of T, the InternalRel of T,CCC #) #) is strict RelStr
the mapping of NetStr(# the carrier of T, the InternalRel of T,CCC #) is Relation-like the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) -defined the carrier of C -valued Function-like V14( the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #)) quasi_total Element of bool [: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of C:]
[: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of C:] is Relation-like set
bool [: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of C:] is non empty set
the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) --> CC is Relation-like the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #) -defined the carrier of C -valued Function-like constant V14( the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #)) quasi_total Element of bool [: the carrier of NetStr(# the carrier of T, the InternalRel of T,CCC #), the carrier of C:]
CCC is strict NetStr over C
the carrier of CCC is set
the InternalRel of CCC is Relation-like the carrier of CCC -defined the carrier of CCC -valued Element of bool [: the carrier of CCC, the carrier of CCC:]
[: the carrier of CCC, the carrier of CCC:] is Relation-like set
bool [: the carrier of CCC, the carrier of CCC:] is non empty set
RelStr(# the carrier of CCC, the InternalRel of CCC #) is strict RelStr
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of C -valued Function-like V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of C:]
[: the carrier of CCC, the carrier of C:] is Relation-like set
bool [: the carrier of CCC, the carrier of C:] is non empty set
the carrier of CCC --> CC is Relation-like the carrier of CCC -defined the carrier of C -valued Function-like constant V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of C:]
C9 is strict NetStr over C
the carrier of C9 is set
the InternalRel of C9 is Relation-like the carrier of C9 -defined the carrier of C9 -valued Element of bool [: the carrier of C9, the carrier of C9:]
[: the carrier of C9, the carrier of C9:] is Relation-like set
bool [: the carrier of C9, the carrier of C9:] is non empty set
RelStr(# the carrier of C9, the InternalRel of C9 #) is strict RelStr
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of C -valued Function-like V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of C:]
[: the carrier of C9, the carrier of C:] is Relation-like set
bool [: the carrier of C9, the carrier of C:] is non empty set
the carrier of C9 --> CC is Relation-like the carrier of C9 -defined the carrier of C -valued Function-like constant V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of C:]
C is non empty 1-sorted
the carrier of C is non empty set
T is RelStr
CC is Element of the carrier of C
(T,C,CC) is strict NetStr over C
the carrier of (T,C,CC) is set
the carrier of (T,C,CC) --> CC is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like constant V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
[: the carrier of (T,C,CC), the carrier of C:] is Relation-like set
bool [: the carrier of (T,C,CC), the carrier of C:] is non empty set
the mapping of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
C is non empty 1-sorted
the carrier of C is non empty set
T is non empty RelStr
CC is Element of the carrier of C
(T,C,CC) is strict (C) NetStr over C
the carrier of (T,C,CC) is set
the InternalRel of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of (T,C,CC) -valued Element of bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):]
[: the carrier of (T,C,CC), the carrier of (T,C,CC):] is Relation-like set
bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):] is non empty set
RelStr(# the carrier of (T,C,CC), the InternalRel of (T,C,CC) #) is strict RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
C is non empty 1-sorted
the carrier of C is non empty set
T is non empty directed RelStr
CC is Element of the carrier of C
(T,C,CC) is non empty strict (C) NetStr over C
the carrier of (T,C,CC) is non empty set
the InternalRel of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of (T,C,CC) -valued Element of bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):]
[: the carrier of (T,C,CC), the carrier of (T,C,CC):] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):] is non empty set
RelStr(# the carrier of (T,C,CC), the InternalRel of (T,C,CC) #) is non empty strict RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
C is non empty 1-sorted
the carrier of C is non empty set
T is non empty transitive RelStr
CC is Element of the carrier of C
(T,C,CC) is non empty strict (C) NetStr over C
the carrier of (T,C,CC) is non empty set
the InternalRel of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of (T,C,CC) -valued Element of bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):]
[: the carrier of (T,C,CC), the carrier of (T,C,CC):] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):] is non empty set
RelStr(# the carrier of (T,C,CC), the InternalRel of (T,C,CC) #) is non empty strict RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
T is RelStr
the carrier of T is set
C is non empty 1-sorted
the carrier of C is non empty set
CC is Element of the carrier of C
(T,C,CC) is strict (C) NetStr over C
the carrier of (T,C,CC) is set
the InternalRel of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of (T,C,CC) -valued Element of bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):]
[: the carrier of (T,C,CC), the carrier of (T,C,CC):] is Relation-like set
bool [: the carrier of (T,C,CC), the carrier of (T,C,CC):] is non empty set
RelStr(# the carrier of (T,C,CC), the InternalRel of (T,C,CC) #) is strict RelStr
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 Relation-like 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
T is non empty RelStr
C is non empty 1-sorted
the carrier of C is non empty set
CC is Element of the carrier of C
(T,C,CC) is non empty strict (C) NetStr over C
the carrier of (T,C,CC) is non empty set
CCC is Element of the carrier of (T,C,CC)
(T,C,CC) . CCC is Element of the carrier of C
the mapping of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like non empty V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
[: the carrier of (T,C,CC), the carrier of C:] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of C:] is non empty set
the mapping of (T,C,CC) . CCC is Element of the carrier of C
the carrier of (T,C,CC) --> CC is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like constant non empty V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
( the carrier of (T,C,CC) --> CC) . CCC is Element of the carrier of C
T is non empty 1-sorted
C is non empty NetStr over T
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of C is non empty set
the carrier of T is non empty set
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
T is RelStr
the carrier of T 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 Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
C is SubRelStr of T
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the InternalRel of T |_2 the carrier of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
the InternalRel of T /\ [: the carrier of C, the carrier of C:] is Relation-like the carrier of T -defined the carrier of T -valued set
T is RelStr
C is SubRelStr of T
CC is SubRelStr of C
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
the carrier of T is set
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
the carrier of CC is set
the InternalRel of CC is Relation-like the carrier of CC -defined the carrier of CC -valued Element of bool [: the carrier of CC, the carrier of CC:]
[: the carrier of CC, the carrier of CC:] is Relation-like set
bool [: the carrier of CC, the carrier of CC:] is non empty set
T is 1-sorted
C is NetStr over T
the carrier of C is set
the carrier of T is set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C | the carrier of C is Relation-like the carrier of C -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
T is 1-sorted
C is NetStr over T
the carrier of C is set
the carrier of T is set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C | the carrier of C is Relation-like the carrier of C -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
T is 1-sorted
C is NetStr over T
CC is (T,C)
CCC is (T,CC)
the carrier of CCC is set
the carrier of CC is set
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
the carrier of T is set
[: the carrier of CCC, the carrier of T:] is Relation-like set
bool [: the carrier of CCC, the carrier of T:] is non empty set
the mapping of CC is Relation-like the carrier of CC -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of CC, the carrier of T:]
[: the carrier of CC, the carrier of T:] is Relation-like set
bool [: the carrier of CC, the carrier of T:] is non empty set
the mapping of CC | the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of CC -defined the carrier of T -valued Function-like Element of bool [: the carrier of CC, the carrier of T:]
the carrier of C is set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C | the carrier of CC is Relation-like the carrier of CC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
( the mapping of C | the carrier of CC) | the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of CC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
the carrier of CC /\ the carrier of CCC is set
the mapping of C | ( the carrier of CC /\ the carrier of CCC) is Relation-like the carrier of C -defined the carrier of CC /\ the carrier of CCC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
the mapping of C | the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
T is 1-sorted
C is NetStr over T
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of T is set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is strict NetStr over T
the mapping of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is Relation-like the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #), the carrier of T:]
the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is set
[: the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #), the carrier of T:] is Relation-like set
bool [: the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #), the carrier of T:] is non empty set
the mapping of C | the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is Relation-like the carrier of C -defined the carrier of NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
T is 1-sorted
C is NetStr over T
T is 1-sorted
C is NetStr over T
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of T is set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is strict NetStr over T
CC is SubRelStr of C
the carrier of CC is set
the InternalRel of CC is Relation-like the carrier of CC -defined the carrier of CC -valued Element of bool [: the carrier of CC, the carrier of CC:]
[: the carrier of CC, the carrier of CC:] is Relation-like set
bool [: the carrier of CC, the carrier of CC:] is non empty set
the InternalRel of C |_2 the carrier of CC is Relation-like the carrier of CC -defined the carrier of CC -valued Element of bool [: the carrier of CC, the carrier of CC:]
the InternalRel of C /\ [: the carrier of CC, the carrier of CC:] is Relation-like the carrier of C -defined the carrier of C -valued set
T is 1-sorted
C is NetStr over T
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of T is set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is strict NetStr over T
CC is (T,C)
T is 1-sorted
C is non empty NetStr over T
the carrier of C is non empty set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of T is set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
NetStr(# the carrier of C, the InternalRel of C, the mapping of C #) is non empty strict NetStr over T
CC is (T,C)
T is 1-sorted
C is NetStr over T
the carrier of C is set
CC is (T,C)
the carrier of CC is set
T is 1-sorted
C is NetStr over T
the carrier of C is set
CC is (T,C)
the carrier of CC is set
CCC is Element of the carrier of C
C9 is Element of the carrier of C
x is Element of the carrier of CC
y is Element of the carrier of CC
M is SubRelStr of C
the carrier of M is set
p is Element of the carrier of M
q is Element of the carrier of M
T is 1-sorted
C is non empty NetStr over T
the carrier of C is non empty set
CC is non empty (T,C) (T,C)
the carrier of CC is non empty set
CCC is Element of the carrier of C
C9 is Element of the carrier of C
x is Element of the carrier of CC
y is Element of the carrier of CC
M is non empty full SubRelStr of C
the carrier of M is non empty set
p is Element of the carrier of M
q is Element of the carrier of M
T is non empty 1-sorted
the non empty transitive directed RelStr is non empty transitive directed RelStr
the carrier of T is non empty set
the Element of the carrier of T is Element of the carrier of T
( the non empty transitive directed RelStr ,T, the Element of the carrier of T) is non empty transitive strict directed (T) NetStr over T
T is non empty 1-sorted
C is (T) NetStr over T
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of C is set
the carrier of T is non empty set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
T is non empty 1-sorted
C is NetStr over T
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of C is set
the carrier of T is non empty set
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
the_value_of the mapping of C is set
CC is non empty (T) NetStr over T
the mapping of CC is Relation-like the carrier of CC -defined the carrier of T -valued Function-like constant non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
the carrier of CC is non empty set
[: the carrier of CC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of T:] is non empty set
dom the mapping of CC is non empty Element of bool the carrier of CC
bool the carrier of CC is non empty set
the_value_of the mapping of CC is set
rng the mapping of CC is non empty trivial 1 -element Element of bool the carrier of T
bool the carrier of T is non empty set
C9 is set
the mapping of CC . C9 is set
T is non empty RelStr
C is non empty 1-sorted
the carrier of C is non empty set
CC is Element of the carrier of C
(T,C,CC) is non empty strict (C) NetStr over C
(C,(T,C,CC)) is Element of the carrier of C
the mapping of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like constant non empty V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
the carrier of (T,C,CC) is non empty set
[: the carrier of (T,C,CC), the carrier of C:] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of C:] is non empty set
the_value_of the mapping of (T,C,CC) is set
the carrier of (T,C,CC) --> CC is Relation-like the carrier of (T,C,CC) -defined the carrier of C -valued Function-like constant non empty V14( the carrier of (T,C,CC)) quasi_total Element of bool [: the carrier of (T,C,CC), the carrier of C:]
the_value_of ( the carrier of (T,C,CC) --> CC) is set
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
the carrier of C is non empty set
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
id C is Relation-like the carrier of C -defined the carrier of C -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of C:]
id the carrier of C is Relation-like the carrier of C -defined the carrier of C -valued Function-like one-to-one non empty V14( the carrier of C) quasi_total onto bijective V35() V37() V38() V42() Element of bool [: the carrier of C, the carrier of C:]
the mapping of C * (id C) is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
CC is Element of the carrier of C
CCC is Element of the carrier of C
C9 is Element of the carrier of C
( the carrier of C,C,(id C),C9) is Element of the carrier of C
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
id C is Relation-like the carrier of C -defined the carrier of C -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of C:]
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
id the carrier of C is Relation-like the carrier of C -defined the carrier of C -valued Function-like one-to-one non empty V14( the carrier of C) quasi_total onto bijective V35() V37() V38() V42() Element of bool [: the carrier of C, the carrier of C:]
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C * (id C) is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
CC is Element of the carrier of C
CCC is Element of the carrier of C
C9 is Element of the carrier of C
( the carrier of C,C,(id C),C9) is Element of the carrier of C
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is non empty transitive directed NetStr over T
CCC is non empty transitive directed NetStr over T
the carrier of C is non empty set
the carrier of CC is non empty set
[: the carrier of C, the carrier of CC:] is Relation-like non empty set
bool [: the carrier of C, the carrier of CC:] is non empty set
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of CC is Relation-like the carrier of CC -defined the carrier of T -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
[: the carrier of CC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of T:] is non empty set
C9 is Relation-like the carrier of C -defined the carrier of CC -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of CC:]
the mapping of CC * C9 is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
the carrier of CCC is non empty set
[: the carrier of CC, the carrier of CCC:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of CCC:] is non empty set
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
[: the carrier of CCC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of T:] is non empty set
x is Relation-like the carrier of CC -defined the carrier of CCC -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of CCC:]
the mapping of CCC * x is Relation-like the carrier of CC -defined the carrier of T -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
x * C9 is Relation-like the carrier of C -defined the carrier of CCC -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of CCC:]
[: the carrier of C, the carrier of CCC:] is Relation-like non empty set
bool [: the carrier of C, the carrier of CCC:] is non empty set
the mapping of CCC * (x * C9) is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
y is Element of the carrier of CCC
M is Element of the carrier of CC
p is Element of the carrier of C
q is Element of the carrier of C
( the carrier of C,CCC,(x * C9),q) is Element of the carrier of CCC
( the carrier of C,CC,C9,q) is Element of the carrier of CC
( the carrier of CC,CCC,x,( the carrier of C,CC,C9,q)) is Element of the carrier of CCC
T is non empty 1-sorted
C is non empty transitive directed (T) NetStr over T
the carrier of C is non empty set
(T,C) is Element of the carrier of T
the carrier of T is non empty set
CC is Element of the carrier of C
C . CC is Element of the carrier of T
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like constant non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C . CC is Element of the carrier of T
dom the mapping of C is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
the_value_of the mapping of C is set
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is set
CCC is set
the carrier of C is non empty set
C9 is Element of the carrier of C
x is Element of the carrier of C
y is Element of the carrier of C
C . y is Element of the carrier of T
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C . y is Element of the carrier of T
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is non empty transitive directed (T,C)
CCC is set
the carrier of C is non empty set
C9 is Element of the carrier of C
the carrier of CC is non empty set
[: the carrier of CC, the carrier of C:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of C:] is non empty set
the carrier of T is non empty set
the mapping of CC is Relation-like the carrier of CC -defined the carrier of T -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
[: the carrier of CC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of T:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
x is Relation-like the carrier of CC -defined the carrier of C -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of C:]
the mapping of C * x is Relation-like the carrier of CC -defined the carrier of T -valued Function-like non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
y is Element of the carrier of CC
M is Element of the carrier of CC
CC . M is Element of the carrier of T
the mapping of CC . M is Element of the carrier of T
( the carrier of CC,C,x,M) is Element of the carrier of C
C . ( the carrier of CC,C,x,M) is Element of the carrier of T
the mapping of C . ( the carrier of CC,C,x,M) is Element of the carrier of T
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is set
the carrier of C is non empty set
CCC is Element of the carrier of C
C9 is Element of the carrier of C
x is Element of the carrier of C
C . x is Element of the carrier of T
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C . x is Element of the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
CCC is Element of the carrier of C
C . CCC is Element of the carrier of T
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C . CCC is Element of the carrier of T
T is 1-sorted
C is NetStr over T
the carrier of C is set
the carrier of T is set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like set
bool [: the carrier of C, the carrier of T:] is non empty set
CC is set
the mapping of C " CC is Element of bool the carrier of C
bool the carrier of C is non empty set
[:( the mapping of C " CC),( the mapping of C " CC):] is Relation-like set
bool [:( the mapping of C " CC),( the mapping of C " CC):] is non empty set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like set
bool [: the carrier of C, the carrier of C:] is non empty set
the InternalRel of C |_2 ( the mapping of C " CC) is Relation-like the mapping of C " CC -defined the mapping of C " CC -valued Element of bool [:( the mapping of C " CC),( the mapping of C " CC):]
the InternalRel of C /\ [:( the mapping of C " CC),( the mapping of C " CC):] is Relation-like the carrier of C -defined the carrier of C -valued set
x is non empty 1-sorted
the carrier of x is non empty set
[:( the mapping of C " CC), the carrier of x:] is Relation-like set
bool [:( the mapping of C " CC), the carrier of x:] is non empty set
the mapping of C | ( the mapping of C " CC) is Relation-like the carrier of C -defined the mapping of C " CC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
C9 is Relation-like the mapping of C " CC -defined the mapping of C " CC -valued Element of bool [:( the mapping of C " CC),( the mapping of C " CC):]
M is Relation-like the mapping of C " CC -defined the carrier of x -valued Function-like V14( the mapping of C " CC) quasi_total Element of bool [:( the mapping of C " CC), the carrier of x:]
NetStr(# ( the mapping of C " CC),C9,M #) is strict NetStr over x
q is strict (T,C)
the carrier of q is set
[:( the mapping of C " CC), the carrier of T:] is Relation-like set
bool [:( the mapping of C " CC), the carrier of T:] is non empty set
C9 is Relation-like the mapping of C " CC -defined the mapping of C " CC -valued Element of bool [:( the mapping of C " CC),( the mapping of C " CC):]
x is Relation-like the mapping of C " CC -defined the carrier of T -valued Function-like quasi_total Element of bool [:( the mapping of C " CC), the carrier of T:]
NetStr(# ( the mapping of C " CC),C9,x #) is strict NetStr over T
the mapping of NetStr(# ( the mapping of C " CC),C9,x #) is Relation-like the carrier of NetStr(# ( the mapping of C " CC),C9,x #) -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of NetStr(# ( the mapping of C " CC),C9,x #), the carrier of T:]
the carrier of NetStr(# ( the mapping of C " CC),C9,x #) is set
[: the carrier of NetStr(# ( the mapping of C " CC),C9,x #), the carrier of T:] is Relation-like set
bool [: the carrier of NetStr(# ( the mapping of C " CC),C9,x #), the carrier of T:] is non empty set
the mapping of C | the carrier of NetStr(# ( the mapping of C " CC),C9,x #) is Relation-like the carrier of C -defined the carrier of NetStr(# ( the mapping of C " CC),C9,x #) -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
M is strict (T,C)
the carrier of M is set
CCC is strict (T,C)
the carrier of CCC is set
C9 is strict (T,C)
the carrier of C9 is set
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
[: the carrier of CCC, the carrier of T:] is Relation-like set
bool [: the carrier of CCC, the carrier of T:] is non empty set
the mapping of C | the carrier of C9 is Relation-like the carrier of C -defined the carrier of C9 -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of C9, the carrier of T:]
[: the carrier of C9, the carrier of T:] is Relation-like set
bool [: the carrier of C9, the carrier of T:] is non empty set
the InternalRel of CCC is Relation-like the carrier of CCC -defined the carrier of CCC -valued Element of bool [: the carrier of CCC, the carrier of CCC:]
[: the carrier of CCC, the carrier of CCC:] is Relation-like set
bool [: the carrier of CCC, the carrier of CCC:] is non empty set
RelStr(# the carrier of CCC, the InternalRel of CCC #) is strict RelStr
the InternalRel of C9 is Relation-like the carrier of C9 -defined the carrier of C9 -valued Element of bool [: the carrier of C9, the carrier of C9:]
[: the carrier of C9, the carrier of C9:] is Relation-like set
bool [: the carrier of C9, the carrier of C9:] is non empty set
RelStr(# the carrier of C9, the InternalRel of C9 #) is strict RelStr
T is 1-sorted
C is transitive NetStr over T
CC is set
(T,C,CC) is strict (T,C)
CCC is transitive full SubRelStr of C
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is set
(T,C,CC) is transitive strict (T,C) (T,C)
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
C9 is Element of the carrier of C
C . C9 is Element of the carrier of T
the carrier of T is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C . C9 is Element of the carrier of T
the mapping of C " CC is Element of bool the carrier of C
bool the carrier of C is non empty set
the carrier of (T,C,CC) is set
x is non empty (T,C) (T,C)
the carrier of x is non empty set
y is Element of the carrier of x
M is Element of the carrier of x
p is Element of the carrier of C
q is Element of the carrier of C
M is Element of the carrier of C
N is Element of the carrier of C
C . N is Element of the carrier of T
the mapping of C . N is Element of the carrier of T
Y is Element of the carrier of x
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is set
(T,C,CC) is transitive strict (T,C) (T,C)
CCC is non empty transitive directed NetStr over T
id CCC is Relation-like the carrier of CCC -defined the carrier of CCC -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of CCC:]
the carrier of CCC is non empty set
[: the carrier of CCC, the carrier of CCC:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of CCC:] is non empty set
id the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of CCC -valued Function-like one-to-one non empty V14( the carrier of CCC) quasi_total onto bijective V35() V37() V38() V42() Element of bool [: the carrier of CCC, the carrier of CCC:]
the carrier of C is non empty set
[: the carrier of CCC, the carrier of C:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of C:] is non empty set
x is Relation-like the carrier of CCC -defined the carrier of C -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of C:]
the carrier of T is non empty set
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
[: the carrier of CCC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of T:] is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C * x is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
the mapping of C | the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
y is Element of the carrier of C
M is Element of the carrier of C
C . M is Element of the carrier of T
the mapping of C . M is Element of the carrier of T
the mapping of C " CC is Element of bool the carrier of C
bool the carrier of C is non empty set
p is Element of the carrier of CCC
q is Element of the carrier of CCC
( the carrier of CCC,C,x,q) is Element of the carrier of C
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
CC is set
(T,C,CC) is transitive strict (T,C) (T,C)
CCC is non empty transitive directed (T,C)
the carrier of CCC is non empty set
the Element of the carrier of CCC is Element of the carrier of CCC
x is Element of the carrier of CCC
CCC . x is Element of the carrier of T
the carrier of T is non empty set
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of T -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of T:]
[: the carrier of CCC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of T:] is non empty set
the mapping of CCC . x is Element of the carrier of T
the carrier of C is non empty set
the mapping of C is Relation-like the carrier of C -defined the carrier of T -valued Function-like non empty V14( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of T:]
[: the carrier of C, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C, the carrier of T:] is non empty set
the mapping of C " CC is Element of bool the carrier of C
bool the carrier of C is non empty set
the mapping of C . x is set
the mapping of C | the carrier of CCC is Relation-like the carrier of CCC -defined the carrier of C -defined the carrier of T -valued Function-like Element of bool [: the carrier of C, the carrier of T:]
T is non empty 1-sorted
the carrier of T is non empty set
( the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
{ NetStr(# a₁,b₁,b₂ #) where b₁ is Relation-like a₁ -defined a₁ -valued Element of bool [:a₁,a₁:], b₂ is Relation-like a₁ -defined the carrier of T -valued Function-like V14(a₁) quasi_total Element of Funcs (a₁, the carrier of T) : NetStr(# a₁,b₁,b₂ #) is non empty transitive directed NetStr over T } is set
CC is Relation-like ( the carrier of T) -defined Function-like non empty V14(( the carrier of T)) set
Union CC is set
CCC is set
C9 is set
proj2 CC is non empty set
union (proj2 CC) is set
x is set
dom CC is non empty Element of bool ( the carrier of T)
bool ( the carrier of T) is non empty set
y is set
CC . y is set
[:y,y:] is Relation-like set
bool [:y,y:] is non empty set
Funcs (y, the carrier of T) is functional non empty FUNCTION_DOMAIN of y, the carrier of T
{ NetStr(# y,b₁,b₂ #) where b₁ is Relation-like y -defined y -valued Element of bool [:y,y:], b₂ is Relation-like y -defined the carrier of T -valued Function-like V14(y) quasi_total Element of Funcs (y, the carrier of T) : NetStr(# y,b₁,b₂ #) is non empty transitive directed NetStr over T } is set
M is Relation-like y -defined y -valued Element of bool [:y,y:]
p is Relation-like y -defined the carrier of T -valued Function-like V14(y) quasi_total Element of Funcs (y, the carrier of T)
NetStr(# y,M,p #) is strict NetStr over T
q is non empty transitive strict directed NetStr over T
M is non empty transitive strict directed NetStr over T
the carrier of M is non empty set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
CC . the carrier of x is set
the mapping of x is Relation-like the carrier of x -defined the carrier of T -valued Function-like non empty V14( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of T:]
[: the carrier of x, the carrier of T:] is Relation-like non empty set
bool [: the carrier of x, the carrier of T:] is non empty set
Funcs ( the carrier of x, the carrier of T) is functional non empty FUNCTION_DOMAIN of the carrier of x, the carrier of T
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
{ NetStr(# the carrier of x,b₁,b₂ #) where b₁ is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:], b₂ is Relation-like the carrier of x -defined the carrier of T -valued Function-like non empty V14( the carrier of x) quasi_total Element of Funcs ( the carrier of x, the carrier of T) : NetStr(# the carrier of x,b₁,b₂ #) is non empty transitive directed NetStr over T } is set
T is non empty 1-sorted
(T) is set
[:{{}},{{}}:] is Relation-like non empty set
bool [:{{}},{{}}:] is non empty set
[{},{}] is V15() set
{{},{}} is functional non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is Relation-like Function-like constant non empty trivial 1 -element set
C is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]
RelStr(# {{}},C #) is non empty trivial V63() 1 -element strict RelStr
the carrier of RelStr(# {{}},C #) is non empty trivial V48() 1 -element countable set
CCC is Element of the carrier of RelStr(# {{}},C #)
C9 is Element of the carrier of RelStr(# {{}},C #)
[CCC,C9] is V15() Element of the carrier of [:RelStr(# {{}},C #),RelStr(# {{}},C #):]
[:RelStr(# {{}},C #),RelStr(# {{}},C #):] is non empty strict RelStr
the carrier of [:RelStr(# {{}},C #),RelStr(# {{}},C #):] is non empty set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
CCC is Element of the carrier of RelStr(# {{}},C #)
C9 is Element of the carrier of RelStr(# {{}},C #)
x is Element of the carrier of RelStr(# {{}},C #)
CCC is Element of the carrier of RelStr(# {{}},C #)
C9 is Element of the carrier of RelStr(# {{}},C #)
the carrier of T is non empty set
( the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
the Element of the carrier of T is Element of the carrier of T
CCC is non empty transitive directed RelStr
(CCC,T, the Element of the carrier of T) is non empty transitive strict directed (T) NetStr over T
the carrier of (CCC,T, the Element of the carrier of T) is non empty set
the InternalRel of (CCC,T, the Element of the carrier of T) is Relation-like the carrier of (CCC,T, the Element of the carrier of T) -defined the carrier of (CCC,T, the Element of the carrier of T) -valued Element of bool [: the carrier of (CCC,T, the Element of the carrier of T), the carrier of (CCC,T, the Element of the carrier of T):]
[: the carrier of (CCC,T, the Element of the carrier of T), the carrier of (CCC,T, the Element of the carrier of T):] is Relation-like non empty set
bool [: the carrier of (CCC,T, the Element of the carrier of T), the carrier of (CCC,T, the Element of the carrier of T):] is non empty set
RelStr(# the carrier of (CCC,T, the Element of the carrier of T), the InternalRel of (CCC,T, the Element of the carrier of T) #) is non empty strict RelStr
the carrier of CCC is non empty set
the InternalRel of CCC is Relation-like the carrier of CCC -defined the carrier of CCC -valued Element of bool [: the carrier of CCC, the carrier of CCC:]
[: the carrier of CCC, the carrier of CCC:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of CCC:] is non empty set
RelStr(# the carrier of CCC, the InternalRel of CCC #) is non empty strict RelStr
T is non empty 1-sorted
the carrier of T is non empty set
C is non empty 1-sorted
the carrier of C is non empty set
CC is non empty transitive directed (T) NetStr over T
the mapping of CC is Relation-like the carrier of CC -defined the carrier of T -valued Function-like constant non empty V14( the carrier of CC) quasi_total Element of bool [: the carrier of CC, the carrier of T:]
the carrier of CC is non empty set
[: the carrier of CC, the carrier of T:] is Relation-like non empty set
bool [: the carrier of CC, the carrier of T:] is non empty set
CCC is non empty transitive directed NetStr over C
the mapping of CCC is Relation-like the carrier of CCC -defined the carrier of C -valued Function-like non empty V14( the carrier of CCC) quasi_total Element of bool [: the carrier of CCC, the carrier of C:]
the carrier of CCC is non empty set
[: the carrier of CCC, the carrier of C:] is Relation-like non empty set
bool [: the carrier of CCC, the carrier of C:] is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
C is non empty 1-sorted
the carrier of C is non empty set
(T) is non empty set
(C) is non empty set
( the carrier of C) is non empty epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of the carrier of C is epsilon-transitive set
Tarski-Class (the_transitive-closure_of the carrier of C) is non empty epsilon-transitive subset-closed Tarski universal set
CC is set
( the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of the carrier of T is epsilon-transitive set
Tarski-Class (the_transitive-closure_of the carrier of T) is non empty epsilon-transitive subset-closed Tarski universal set
CCC is non empty transitive strict directed NetStr over T
the carrier of CCC is non empty set
C9 is non empty transitive strict directed NetStr over C
the carrier of C9 is non empty set
CCC is non empty transitive strict directed NetStr over C
the carrier of CCC is non empty set
CCC is non empty transitive strict directed NetStr over C
the carrier of CCC is non empty set
C9 is non empty transitive strict directed NetStr over T
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
CC is set
C9 is non empty transitive strict directed NetStr over C
CCC is set
the carrier of C9 is non empty set
T is set
C is 1-sorted
the non empty transitive directed NetStr over C is non empty transitive directed NetStr over C
T --> the non empty transitive directed NetStr over C is Relation-like T -defined { the non empty transitive directed NetStr over C} -valued Function-like constant V14(T) quasi_total 1-sorted-yielding RelStr-yielding Element of bool [:T,{ the non empty transitive directed NetStr over C}:]
{ the non empty transitive directed NetStr over C} is non empty trivial 1 -element set
[:T,{ the non empty transitive directed NetStr over C}:] is Relation-like set
bool [:T,{ the non empty transitive directed NetStr over C}:] is non empty set
proj2 (T --> the non empty transitive directed NetStr over C) is trivial set
CCC is set
rng (T --> the non empty transitive directed NetStr over C) is trivial Element of bool { the non empty transitive directed NetStr over C}
bool { the non empty transitive directed NetStr over C} is non empty set
T is set
C is 1-sorted
CC is Relation-like T -defined Function-like V14(T) set
CCC is set
dom CC is Element of bool T
bool T is non empty set
CC . CCC is set
proj2 CC is set
CCC is set
C9 is set
CC . C9 is set
T is non empty set
C is 1-sorted
CC is Relation-like T -defined Function-like non empty V14(T) (T,C)
CCC is Element of T
CC . CCC is set
T is set
C is 1-sorted
CC is Relation-like T -defined Function-like V14(T) (T,C)
CCC is set
proj2 CC is set
T is 1-sorted
C is non empty transitive directed NetStr over T
the carrier of C is non empty set
CC is Relation-like the carrier of C -defined Function-like non empty V14( the carrier of C) 1-sorted-yielding RelStr-yielding ( the carrier of C,T)
CCC is set
proj2 CC is non empty set
T is non empty 1-sorted
C is non empty transitive directed NetStr over T
the carrier of C is non empty set
CC is Relation-like the carrier of C -defined Function-like non empty V14( the carrier of C) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of C,T)
product CC is non empty strict RelStr
the carrier of (product CC) is