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

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

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

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