:: 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 functional non empty set
Carrier CC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
product (Carrier CC) is functional non empty with_common_domain product-like set
CCC is Relation-like Function-like Element of the carrier of (product CC)
C9 is Relation-like Function-like Element of the carrier of (product CC)
x is Element of the carrier of C
( the carrier of C,T,CC,x) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CC,x) is non empty set
CCC . x is Element of the carrier of (CC . x)
CC . x is non empty RelStr
the carrier of (CC . x) is non empty set
C9 . x is Element of the carrier of (CC . x)
y is Element of the carrier of ( the carrier of C,T,CC,x)
M is set
p is set
[(CCC . x),p] is V15() set
{(CCC . x),p} is non empty set
{(CCC . x)} is non empty trivial 1 -element set
{{(CCC . x),p},{(CCC . x)}} is non empty set
the InternalRel of ( the carrier of C,T,CC,x) is Relation-like the carrier of ( the carrier of C,T,CC,x) -defined the carrier of ( the carrier of C,T,CC,x) -valued Element of bool [: the carrier of ( the carrier of C,T,CC,x), the carrier of ( the carrier of C,T,CC,x):]
[: the carrier of ( the carrier of C,T,CC,x), the carrier of ( the carrier of C,T,CC,x):] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,x), the carrier of ( the carrier of C,T,CC,x):] is non empty set
[(C9 . x),p] is V15() set
{(C9 . x),p} is non empty set
{(C9 . x)} is non empty trivial 1 -element set
{{(C9 . x),p},{(C9 . x)}} is non empty set
x is Relation-like the carrier of C -defined Function-like non empty V14( the carrier of C) set
y is set
dom (Carrier CC) is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
M is Element of the carrier of C
CCC . M is Element of the carrier of (CC . M)
CC . M is non empty RelStr
the carrier of (CC . M) is non empty set
x . M is set
[(CCC . M),(x . M)] is V15() set
{(CCC . M),(x . M)} is non empty set
{(CCC . M)} is non empty trivial 1 -element set
{{(CCC . M),(x . M)},{(CCC . M)}} is non empty set
( the carrier of C,T,CC,M) is non empty transitive directed NetStr over T
the InternalRel of ( the carrier of C,T,CC,M) is Relation-like the carrier of ( the carrier of C,T,CC,M) -defined the carrier of ( the carrier of C,T,CC,M) -valued Element of bool [: the carrier of ( the carrier of C,T,CC,M), the carrier of ( the carrier of C,T,CC,M):]
the carrier of ( the carrier of C,T,CC,M) is non empty set
[: the carrier of ( the carrier of C,T,CC,M), the carrier of ( the carrier of C,T,CC,M):] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,M), the carrier of ( the carrier of C,T,CC,M):] is non empty set
x . y is set
(Carrier CC) . y is set
dom x is non empty Element of bool the carrier of C
y is Relation-like Function-like Element of the carrier of (product CC)
M is set
CC . M is set
CCC . M is set
y . M is set
p is Element of the carrier of C
( the carrier of C,T,CC,p) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CC,p) is non empty set
CCC . p is Element of the carrier of (CC . p)
CC . p is non empty RelStr
the carrier of (CC . p) is non empty set
y . p is Element of the carrier of (CC . p)
q is Element of the carrier of ( the carrier of C,T,CC,p)
M is Element of the carrier of ( the carrier of C,T,CC,p)
[q,M] is V15() Element of the carrier of [:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):]
[:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):] is non empty strict transitive directed RelStr
the carrier of [:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):] is non empty set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
the InternalRel of ( the carrier of C,T,CC,p) is Relation-like the carrier of ( the carrier of C,T,CC,p) -defined the carrier of ( the carrier of C,T,CC,p) -valued Element of bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):]
[: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):] is non empty set
M is set
CC . M is set
C9 . M is set
y . M is set
p is Element of the carrier of C
( the carrier of C,T,CC,p) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CC,p) is non empty set
C9 . p is Element of the carrier of (CC . p)
CC . p is non empty RelStr
the carrier of (CC . p) is non empty set
y . p is Element of the carrier of (CC . p)
q is Element of the carrier of ( the carrier of C,T,CC,p)
M is Element of the carrier of ( the carrier of C,T,CC,p)
[q,M] is V15() Element of the carrier of [:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):]
[:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):] is non empty strict transitive directed RelStr
the carrier of [:( the carrier of C,T,CC,p),( the carrier of C,T,CC,p):] is non empty set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
the InternalRel of ( the carrier of C,T,CC,p) is Relation-like the carrier of ( the carrier of C,T,CC,p) -defined the carrier of ( the carrier of C,T,CC,p) -valued Element of bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):]
[: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of ( the carrier of C,T,CC,p):] is non empty set
CCC is Relation-like Function-like Element of the carrier of (product CC)
C9 is Relation-like Function-like Element of the carrier of (product CC)
x is Relation-like Function-like Element of the carrier of (product CC)
y is set
CC . y is set
CCC . y is set
x . y is set
C9 . y is set
p is Relation-like Function-like set
q is Relation-like Function-like set
p is RelStr
the carrier of p is set
q is Element of the carrier of p
M is Element of the carrier of p
N is Relation-like Function-like set
Y is Relation-like Function-like set
N is RelStr
the carrier of N is set
Y is Element of the carrier of N
Y9 is Element of the carrier of N
M is Element of the carrier of C
( the carrier of C,T,CC,M) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CC,M) is non empty set
YY is Element of the carrier of ( the carrier of C,T,CC,M)
X is Element of the carrier of ( the carrier of C,T,CC,M)
T is set
C is 1-sorted
CC is Relation-like T -defined Function-like V14(T) 1-sorted-yielding RelStr-yielding (T,C)
CCC is set
proj2 CC is set
T is set
C is 1-sorted
the Relation-like T -defined Function-like V14(T) 1-sorted-yielding RelStr-yielding non-Empty (T,C) is Relation-like T -defined Function-like V14(T) 1-sorted-yielding RelStr-yielding non-Empty (T,C)
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 transitive directed RelStr
[:C,(product CC):] is non empty strict transitive directed RelStr
the carrier of (product CC) is functional non empty set
the carrier of T is non empty set
C9 is Element of the carrier of C
CC . C9 is non empty RelStr
the carrier of (CC . C9) is non empty set
( the carrier of C,T,CC,C9) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C,T,CC,C9) is Relation-like the carrier of ( the carrier of C,T,CC,C9) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,C9)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,C9), the carrier of T:]
the carrier of ( the carrier of C,T,CC,C9) is non empty set
[: the carrier of ( the carrier of C,T,CC,C9), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,C9), the carrier of T:] is non empty set
x is Relation-like Function-like Element of the carrier of (product CC)
x . C9 is Element of the carrier of (CC . C9)
the mapping of ( the carrier of C,T,CC,C9) . (x . C9) is Element of the carrier of T
[: the carrier of C, the carrier of (product CC):] is Relation-like non empty set
[:[: the carrier of C, the carrier of (product CC):], the carrier of T:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of (product CC):], the carrier of T:] is non empty set
C9 is Relation-like [: the carrier of C, the carrier of (product CC):] -defined the carrier of T -valued Function-like non empty V14([: the carrier of C, the carrier of (product CC):]) quasi_total Element of bool [:[: the carrier of C, the carrier of (product CC):], the carrier of T:]
the carrier of [:C,(product CC):] is non empty set
[: the carrier of [:C,(product CC):], the carrier of T:] is Relation-like non empty set
bool [: the carrier of [:C,(product CC):], the carrier of T:] is non empty set
the InternalRel of [:C,(product CC):] is Relation-like the carrier of [:C,(product CC):] -defined the carrier of [:C,(product CC):] -valued Element of bool [: the carrier of [:C,(product CC):], the carrier of [:C,(product CC):]:]
[: the carrier of [:C,(product CC):], the carrier of [:C,(product CC):]:] is Relation-like non empty set
bool [: the carrier of [:C,(product CC):], the carrier of [:C,(product CC):]:] is non empty set
x is Relation-like the carrier of [:C,(product CC):] -defined the carrier of T -valued Function-like non empty V14( the carrier of [:C,(product CC):]) quasi_total Element of bool [: the carrier of [:C,(product CC):], the carrier of T:]
NetStr(# the carrier of [:C,(product CC):], the InternalRel of [:C,(product CC):],x #) is non empty strict NetStr over T
y is non empty transitive strict directed NetStr over T
the carrier of y is non empty set
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
RelStr(# the carrier of y, the InternalRel of y #) is non empty strict RelStr
the mapping of y is Relation-like the carrier of y -defined the carrier of T -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is Relation-like non empty set
bool [: the carrier of y, the carrier of T:] is non empty set
M is Element of the carrier of C
( the carrier of C,T,CC,M) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C,T,CC,M) is Relation-like the carrier of ( the carrier of C,T,CC,M) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,M)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,M), the carrier of T:]
the carrier of ( the carrier of C,T,CC,M) is non empty set
[: the carrier of ( the carrier of C,T,CC,M), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,M), the carrier of T:] is non empty set
p is Relation-like Function-like set
the mapping of y . (M,p) is set
[M,p] is V15() set
{M,p} is non empty set
{M} is non empty trivial 1 -element set
{{M,p},{M}} is non empty set
the mapping of y . [M,p] is set
p . M is set
the mapping of ( the carrier of C,T,CC,M) . (p . M) is set
CCC is non empty transitive strict directed NetStr over T
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
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 T is non empty set
[: 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
C9 is non empty transitive strict directed NetStr over T
the carrier of C9 is non empty 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 non empty set
bool [: the carrier of C9, the carrier of C9:] is non empty set
RelStr(# the carrier of C9, the InternalRel of C9 #) is non empty strict RelStr
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like non empty V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of T:]
[: the carrier of C9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C9, the carrier of T:] is non empty set
the carrier of RelStr(# the carrier of C9, the InternalRel of C9 #) is non empty set
[: the carrier of C, the carrier of (product CC):] is Relation-like non empty set
[:[: the carrier of C, the carrier of (product CC):], the carrier of T:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of (product CC):], the carrier of T:] is non empty set
M is Element of [: the carrier of C, the carrier of (product CC):]
p is Element of the carrier of C
q is Relation-like Function-like Element of the carrier of (product CC)
[p,q] is V15() Element of the carrier of [:C,(product CC):]
the carrier of [:C,(product CC):] is non empty set
{p,q} is non empty set
{p} is non empty trivial 1 -element set
{{p,q},{p}} is non empty set
Carrier CC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
product (Carrier CC) is functional non empty with_common_domain product-like set
x is Relation-like [: the carrier of C, the carrier of (product CC):] -defined the carrier of T -valued Function-like non empty V14([: the carrier of C, the carrier of (product CC):]) quasi_total Element of bool [:[: the carrier of C, the carrier of (product CC):], the carrier of T:]
x . M is Element of the carrier of T
M is Relation-like the carrier of C -defined Function-like Carrier CC -compatible non empty V14( the carrier of C) Element of product (Carrier CC)
x . (p,M) is set
[p,M] is V15() set
{p,M} is non empty set
{{p,M},{p}} is non empty set
x . [p,M] is set
( the carrier of C,T,CC,p) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C,T,CC,p) is Relation-like the carrier of ( the carrier of C,T,CC,p) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,p)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of T:]
the carrier of ( the carrier of C,T,CC,p) is non empty set
[: the carrier of ( the carrier of C,T,CC,p), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of T:] is non empty set
M . p is set
the mapping of ( the carrier of C,T,CC,p) . (M . p) is set
y is Relation-like [: the carrier of C, the carrier of (product CC):] -defined the carrier of T -valued Function-like non empty V14([: the carrier of C, the carrier of (product CC):]) quasi_total Element of bool [:[: the carrier of C, the carrier of (product CC):], the carrier of T:]
y . (p,M) is set
y . [p,M] is set
y . M is Element of the carrier of T
T is non empty 1-sorted
(T) is non empty set
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)
(T,C,CC) is non empty transitive strict directed NetStr over T
Carrier CC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
proj2 (Carrier CC) is non empty with_non-empty_elements set
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
CCC is set
dom (Carrier CC) is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
C9 is set
(Carrier CC) . C9 is set
x is Element of the carrier of C
( the carrier of C,T,CC,x) is non empty transitive directed NetStr over T
y is non empty transitive strict directed NetStr over T
the carrier of y is non empty set
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
product CC is non empty strict transitive directed RelStr
[:C,(product CC):] is non empty strict transitive directed RelStr
the carrier of (product CC) is functional non empty set
[: the carrier of C, the carrier of (product CC):] is Relation-like non empty set
dom (Carrier CC) is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
CCC is non empty transitive strict directed NetStr over T
the carrier of CCC is non empty set
product (Carrier CC) is functional non empty with_common_domain product-like set
CCC is non empty transitive strict directed NetStr over T
the carrier of CCC 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)
(T,C,CC) is non empty transitive strict directed NetStr over T
the carrier of (T,C,CC) is non empty set
Carrier CC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
product (Carrier CC) is functional non empty with_common_domain product-like set
[: the carrier of C,(product (Carrier CC)):] is Relation-like 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
product CC is non empty strict transitive directed RelStr
[:C,(product CC):] is non empty strict transitive directed RelStr
the carrier of (product CC) is functional non empty set
[: the carrier of C, the carrier of (product CC):] is Relation-like non empty set
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
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 transitive directed RelStr
the carrier of (product CC) is functional non empty set
(T,C,CC) is non empty transitive strict directed NetStr over T
the carrier of (T,C,CC) is non empty set
CCC is Element of the carrier of C
CC . CCC is non empty RelStr
the carrier of (CC . CCC) is non empty set
( the carrier of C,T,CC,CCC) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C,T,CC,CCC) is Relation-like the carrier of ( the carrier of C,T,CC,CCC) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,CCC)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,CCC), the carrier of T:]
the carrier of ( the carrier of C,T,CC,CCC) is non empty set
[: the carrier of ( the carrier of C,T,CC,CCC), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,CCC), the carrier of T:] is non empty set
C9 is Relation-like Function-like Element of the carrier of (product CC)
[CCC,C9] is V15() Element of the carrier of [:C,(product CC):]
[:C,(product CC):] is non empty strict transitive directed RelStr
the carrier of [:C,(product CC):] 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
C9 . CCC is Element of the carrier of (CC . CCC)
the mapping of ( the carrier of C,T,CC,CCC) . (C9 . CCC) is Element of the carrier of T
x is Element of the carrier of (T,C,CC)
(T,C,CC) . x is Element of the carrier of T
the mapping of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of T -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 T:]
[: the carrier of (T,C,CC), the carrier of T:] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of T:] is non empty set
the mapping of (T,C,CC) . x is Element of the carrier of T
the mapping of (T,C,CC) . (CCC,C9) is set
[CCC,C9] is V15() set
the mapping of (T,C,CC) . [CCC,C9] is set
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
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)
(T,C,CC) is non empty transitive strict directed NetStr over T
the mapping of (T,C,CC) is Relation-like the carrier of (T,C,CC) -defined the carrier of T -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 T:]
the carrier of (T,C,CC) is non empty set
[: the carrier of (T,C,CC), the carrier of T:] is Relation-like non empty set
bool [: the carrier of (T,C,CC), the carrier of T:] is non empty set
rng the mapping of (T,C,CC) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
{ (rng the mapping of ( the carrier of C,T,CC,b₁)) where b₁ is Element of the carrier of C : verum } is set
union { (rng the mapping of ( the carrier of C,T,CC,b₁)) where b₁ is Element of the carrier of C : verum } is set
CCC is set
dom the mapping of (T,C,CC) is non empty Element of bool the carrier of (T,C,CC)
bool the carrier of (T,C,CC) is non empty set
x is set
the mapping of (T,C,CC) . x is set
Carrier CC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
product (Carrier CC) is functional non empty with_common_domain product-like set
[: the carrier of C,(product (Carrier CC)):] is Relation-like non empty set
y is Element of the carrier of C
M is Relation-like the carrier of C -defined Function-like Carrier CC -compatible non empty V14( the carrier of C) Element of product (Carrier CC)
[y,M] is V15() set
{y,M} is non empty set
{y} is non empty trivial 1 -element set
{{y,M},{y}} is non empty set
dom (Carrier CC) is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
M . y is set
(Carrier CC) . y is non empty set
( the carrier of C,T,CC,y) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CC,y) is non empty set
the mapping of ( the carrier of C,T,CC,y) is Relation-like the carrier of ( the carrier of C,T,CC,y) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,y)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,y), the carrier of T:]
[: the carrier of ( the carrier of C,T,CC,y), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,y), the carrier of T:] is non empty set
dom the mapping of ( the carrier of C,T,CC,y) is non empty Element of bool the carrier of ( the carrier of C,T,CC,y)
bool the carrier of ( the carrier of C,T,CC,y) is non empty set
product CC is non empty strict transitive directed RelStr
the carrier of (product CC) is functional non empty set
the mapping of (T,C,CC) . (y,M) is set
the mapping of (T,C,CC) . [y,M] is set
the mapping of ( the carrier of C,T,CC,y) . (M . y) is set
rng the mapping of ( the carrier of C,T,CC,y) is non empty Element of bool the carrier of T
p is Element of the carrier of C
( the carrier of C,T,CC,p) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C,T,CC,p) is Relation-like the carrier of ( the carrier of C,T,CC,p) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CC,p)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of T:]
the carrier of ( the carrier of C,T,CC,p) is non empty set
[: the carrier of ( the carrier of C,T,CC,p), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CC,p), the carrier of T:] is non empty set
rng the mapping of ( the carrier of C,T,CC,p) is non empty Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
C is Element of the carrier of T
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is Element of the carrier of T
(T,C) is RelStr
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
[#] T is non empty non proper open dense non boundary Element of bool the carrier of T
the carrier of (InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is set
the carrier of (T,C) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
C is Element of the carrier of T
(T,C) is non empty RelStr
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
the carrier of (T,C) is non empty set
CC is Element of the carrier of (T,C)
the carrier of ((InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~) is set
the carrier of (InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
C is Element of the carrier of T
(T,C) is non empty RelStr
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
the carrier of (T,C) is non empty set
CC is Element of bool the carrier of T
C9 is Element of bool the carrier of T
x is Element of bool the carrier of T
the carrier of (InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is Element of the carrier of T
(T,C) is non empty RelStr
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
the carrier of (T,C) is non empty set
[#] T is non empty non proper open dense non boundary Element of bool the carrier of T
C9 is Element of the carrier of (T,C)
x is Element of the carrier of (T,C)
CCC is non empty set
InclPoset CCC is non empty strict V97() reflexive transitive antisymmetric non void RelStr
K386(CCC) is Relation-like CCC -defined CCC -valued V14(CCC) quasi_total V35() V38() V42() Element of bool [:CCC,CCC:]
[:CCC,CCC:] is Relation-like non empty set
bool [:CCC,CCC:] is non empty set
RelStr(# CCC,K386(CCC) #) is non empty strict V97() reflexive transitive antisymmetric non void RelStr
(InclPoset CCC) ~ is non empty strict V97() reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset CCC) is non empty set
the InternalRel of (InclPoset CCC) is Relation-like the carrier of (InclPoset CCC) -defined the carrier of (InclPoset CCC) -valued non empty V14( the carrier of (InclPoset CCC)) quasi_total V35() V38() V42() Element of bool [: the carrier of (InclPoset CCC), the carrier of (InclPoset CCC):]
[: the carrier of (InclPoset CCC), the carrier of (InclPoset CCC):] is Relation-like non empty set
bool [: the carrier of (InclPoset CCC), the carrier of (InclPoset CCC):] is non empty set
the InternalRel of (InclPoset CCC) ~ is Relation-like the carrier of (InclPoset CCC) -defined the carrier of (InclPoset CCC) -valued V14( the carrier of (InclPoset CCC)) quasi_total V35() V38() V42() Element of bool [: the carrier of (InclPoset CCC), the carrier of (InclPoset CCC):]
RelStr(# the carrier of (InclPoset CCC),( the InternalRel of (InclPoset CCC) ~) #) is non empty strict V97() reflexive transitive antisymmetric non void RelStr
M is Element of the carrier of (InclPoset CCC)
y is Element of the carrier of (InclPoset CCC)
y ~ is Element of the carrier of ((InclPoset CCC) ~)
the carrier of ((InclPoset CCC) ~) is non empty set
M ~ is Element of the carrier of ((InclPoset CCC) ~)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is Element of the carrier of T
(T,C) is non empty RelStr
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
the carrier of (T,C) is non empty set
CC is Element of the carrier of (T,C)
CCC is Element of the carrier of (T,C)
x is Element of bool the carrier of T
y is Element of bool the carrier of T
x /\ y is Element of bool the carrier of T
p is Element of the carrier of (T,C)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
bool the carrier of T is non empty set
CC is Element of bool the carrier of T
CCC is Element of the carrier of T
C9 is a_neighborhood of CCC
CC is Element of bool the carrier of T
CCC is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
CC is non empty transitive directed (T,C)
(T,CC) is Element of bool the carrier of T
CCC is set
the carrier of CC is non empty set
the carrier of C 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 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
C9 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 * C9 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 is Element of the carrier of T
y is a_neighborhood of x
M is Element of the carrier of C
p is Element of the carrier of CC
q is Element of the carrier of CC
CC . q is Element of the carrier of T
the mapping of CC . q is Element of the carrier of T
( the carrier of CC,C,C9,q) is Element of the carrier of C
C . ( the carrier of CC,C,C9,q) is Element of the carrier of T
the mapping of C . ( the carrier of CC,C,C9,q) is Element of the carrier of T
T is non empty TopSpace-like TopStruct
C is non empty transitive directed (T) NetStr over T
(T,C) is Element of the carrier of T
the carrier of T is non empty set
(T,C) is Element of bool the carrier of T
bool the carrier of T is non empty set
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
C9 is a_neighborhood of (T,C)
x is Element of the carrier of C
C . x 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 . x is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
the carrier of C is non empty set
CC is Element of the carrier of T
CCC is Element of the carrier of C
{ (C . b₁) where b₁ is Element of the carrier of C : CCC <= b₁ } is set
C9 is set
x is Element of the carrier of C
C . x 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 . x is Element of the carrier of T
C9 is Element of bool the carrier of T
Cl C9 is closed Element of bool the carrier of T
x is a_neighborhood of CC
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 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 . M is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
bool the carrier of T is non empty set
CC is Element of the carrier of T
CCC is Element of the carrier of T
C9 is Element of bool the carrier of T
x is 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
(T,C) is non empty transitive directed RelStr
{ b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( C in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
(T,CC) is non empty transitive directed RelStr
{ b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } is set
InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } is strict V97() reflexive transitive antisymmetric RelStr
K386( { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } ) is Relation-like { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } -defined { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } -valued V14( { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } ) quasi_total V35() V38() V42() Element of bool [: { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } :]
[: { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } :] is Relation-like set
bool [: { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } , { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } :] is non empty set
RelStr(# { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } ,K386( { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } ) #) is strict V97() reflexive transitive antisymmetric RelStr
(InclPoset { b₁ where b₁ is Element of bool the carrier of T : ( CC in b₁ & b₁ is open ) } ) ~ is strict V97() reflexive transitive antisymmetric RelStr
[:(T,C),(T,CC):] is non empty strict transitive directed RelStr
the carrier of [:(T,C),(T,CC):] is non empty set
y is Element of the carrier of [:(T,C),(T,CC):]
y `1 is Element of the carrier of (T,C)
the carrier of (T,C) is non empty set
y `2 is Element of the carrier of (T,CC)
the carrier of (T,CC) is non empty set
(y `1) /\ (y `2) is set
M is Element of bool the carrier of T
p is Element of bool the carrier of T
M /\ p is Element of bool the carrier of T
the carrier of T /\ ((y `1) /\ (y `2)) is set
[: the carrier of [:(T,C),(T,CC):], the carrier of T:] is Relation-like non empty set
bool [: the carrier of [:(T,C),(T,CC):], the carrier of T:] is non empty set
y is Relation-like the carrier of [:(T,C),(T,CC):] -defined the carrier of T -valued Function-like non empty V14( the carrier of [:(T,C),(T,CC):]) quasi_total Element of bool [: the carrier of [:(T,C),(T,CC):], the carrier of T:]
the InternalRel of [:(T,C),(T,CC):] is Relation-like the carrier of [:(T,C),(T,CC):] -defined the carrier of [:(T,C),(T,CC):] -valued Element of bool [: the carrier of [:(T,C),(T,CC):], the carrier of [:(T,C),(T,CC):]:]
[: the carrier of [:(T,C),(T,CC):], the carrier of [:(T,C),(T,CC):]:] is Relation-like non empty set
bool [: the carrier of [:(T,C),(T,CC):], the carrier of [:(T,C),(T,CC):]:] is non empty set
NetStr(# the carrier of [:(T,C),(T,CC):], the InternalRel of [:(T,C),(T,CC):],y #) is non empty strict NetStr over T
the carrier of (T,C) is non empty set
the carrier of (T,CC) is non empty set
[: the carrier of (T,C), the carrier of (T,CC):] is Relation-like non empty set
M is non empty transitive directed NetStr over T
p is a_neighborhood of CC
Int p is open Element of bool the carrier of T
[#] T is non empty non proper open dense non boundary Element of bool the carrier of T
the carrier of M is non empty set
[([#] T),(Int p)] is V15() set
{([#] T),(Int p)} is non empty set
{([#] T)} is non empty trivial 1 -element set
{{([#] T),(Int p)},{([#] T)}} is non empty set
q is Element of the carrier of M
M is Element of the carrier of M
M . M is Element of the carrier of T
the mapping of M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
[: the carrier of M, the carrier of T:] is Relation-like non empty set
bool [: the carrier of M, the carrier of T:] is non empty set
the mapping of M . M is Element of the carrier of T
Y9 is Element of the carrier of (T,C)
YY is Element of the carrier of (T,CC)
[Y9,YY] is V15() Element of the carrier of [:(T,C),(T,CC):]
{Y9,YY} is non empty set
{Y9} is non empty trivial 1 -element set
{{Y9,YY},{Y9}} is non empty set
M `2 is set
X is Element of bool the carrier of T
X is Element of bool the carrier of T
[q,M] is V15() Element of the carrier of [:M,M:]
[:M,M:] is non empty strict transitive directed RelStr
the carrier of [:M,M:] is non empty set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
Y is Element of the carrier of [:(T,C),(T,CC):]
N is Element of the carrier of [:(T,C),(T,CC):]
Y `2 is Element of the carrier of (T,CC)
N `2 is Element of the carrier of (T,CC)
X /\ X is Element of bool the carrier of T
(Int p) /\ ([#] T) is open Element of bool the carrier of T
M `1 is set
y . M is set
(T,M) is Element of bool the carrier of T
p is a_neighborhood of C
Int p is open Element of bool the carrier of T
[#] T is non empty non proper open dense non boundary Element of bool the carrier of T
the carrier of M is non empty set
[(Int p),([#] T)] is V15() set
{(Int p),([#] T)} is non empty set
{(Int p)} is non empty trivial 1 -element set
{{(Int p),([#] T)},{(Int p)}} is non empty set
q is Element of the carrier of M
M is Element of the carrier of M
M . M is Element of the carrier of T
the mapping of M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
[: the carrier of M, the carrier of T:] is Relation-like non empty set
bool [: the carrier of M, the carrier of T:] is non empty set
the mapping of M . M is Element of the carrier of T
Y9 is Element of the carrier of (T,C)
YY is Element of the carrier of (T,CC)
[Y9,YY] is V15() Element of the carrier of [:(T,C),(T,CC):]
{Y9,YY} is non empty set
{Y9} is non empty trivial 1 -element set
{{Y9,YY},{Y9}} is non empty set
M `1 is set
X is Element of bool the carrier of T
X is Element of bool the carrier of T
[q,M] is V15() Element of the carrier of [:M,M:]
[:M,M:] is non empty strict transitive directed RelStr
the carrier of [:M,M:] is non empty set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
Y is Element of the carrier of [:(T,C),(T,CC):]
N is Element of the carrier of [:(T,C),(T,CC):]
Y `1 is Element of the carrier of (T,C)
N `1 is Element of the carrier of (T,C)
X /\ X is Element of bool the carrier of T
(Int p) /\ ([#] T) is open Element of bool the carrier of T
M `2 is set
y . M is set
T is non empty TopSpace-like Hausdorff TopStruct
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
CC is Element of the carrier of T
CCC is Element of the carrier of T
T is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
T is non empty TopSpace-like TopStruct
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) (T) NetStr over T
T is non empty TopSpace-like Hausdorff TopStruct
the carrier of T is non empty set
C is non empty transitive directed (T) NetStr over T
(T,C) is trivial Element of bool the carrier of T
bool the carrier of T is non empty set
CC 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 non empty TopSpace-like Hausdorff TopStruct
C is non empty transitive directed (T) (T) NetStr over T
(T,C) is Element of the carrier of T
the carrier of T is non empty set
(T,C) is Element of the carrier of T
(T,C) is trivial Element of bool the carrier of T
bool the carrier of T is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
bool the carrier of T is non empty set
CC is Element of the carrier of T
CCC is a_neighborhood of CC
the carrier of T \ CCC is Element of bool the carrier of T
(T,C,( the carrier of T \ CCC)) is transitive strict (T,C) (T,C)
C9 is non empty transitive directed (T,C)
x is non empty transitive directed (T,C9)
(T,x) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
(T) is non empty set
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
bool 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
CC is Element of the carrier of T
CCC is a_neighborhood of CC
the carrier of T \ CCC is Element of bool the carrier of T
(T,C,( the carrier of T \ CCC)) is transitive strict (T,C) (T,C)
C9 is non empty transitive directed (T,C)
the carrier of C9 is non empty set
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 " ( the carrier of T \ CCC) is Element of bool the carrier of C
bool the carrier of C is non empty set
x is non empty transitive strict directed NetStr over T
the carrier of x is non empty set
x is non empty transitive directed (T,C9)
(T,x) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
C is non empty transitive directed NetStr over T
(T,C) is Element of bool the carrier of T
bool the carrier of T is non empty set
the carrier of C is non empty set
CC is Element of the carrier of T
CCC 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)
(T,C,CCC) is non empty transitive strict directed NetStr over T
(T,(T,C,CCC)) is Element of bool the carrier of T
C9 is a_neighborhood of CC
Int C9 is open Element of bool the carrier of T
Int (Int C9) is open Element of bool the carrier of T
x is a_neighborhood of CC
y is Element of the carrier of C
M is Element of the carrier of C
( the carrier of C,T,CCC,M) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CCC,M) is non empty set
p is Element of the carrier of C
C . p 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 . p is Element of the carrier of T
C . M is Element of the carrier of T
the mapping of C . M is Element of the carrier of T
(T,( the carrier of C,T,CCC,M)) is Element of bool the carrier of T
q is Element of the carrier of ( the carrier of C,T,CCC,M)
M is Element of the carrier of ( the carrier of C,T,CCC,M)
( the carrier of C,T,CCC,M) . M is Element of the carrier of T
the mapping of ( the carrier of C,T,CCC,M) is Relation-like the carrier of ( the carrier of C,T,CCC,M) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CCC,M)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:]
[: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:] is non empty set
the mapping of ( the carrier of C,T,CCC,M) . M is Element of the carrier of T
the Element of the carrier of ( the carrier of C,T,CCC,M) is Element of the carrier of ( the carrier of C,T,CCC,M)
M is Element of the carrier of ( the carrier of C,T,CCC,M)
( the carrier of C,T,CCC,M) . M is Element of the carrier of T
the mapping of ( the carrier of C,T,CCC,M) is Relation-like the carrier of ( the carrier of C,T,CCC,M) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CCC,M)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:]
[: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CCC,M), the carrier of T:] is non empty set
the mapping of ( the carrier of C,T,CCC,M) . M is Element of the carrier of T
M is Relation-like the carrier of C -defined Function-like non empty V14( the carrier of C) set
Carrier CCC is Relation-like non-empty non empty-yielding the carrier of C -defined Function-like non empty V14( the carrier of C) set
dom (Carrier CCC) is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
p is set
M . p is set
(Carrier CCC) . p is set
q is Element of the carrier of C
( the carrier of C,T,CCC,q) is non empty transitive directed NetStr over T
the carrier of ( the carrier of C,T,CCC,q) is non empty set
M . q is set
M is Element of the carrier of ( the carrier of C,T,CCC,q)
dom M is non empty Element of bool the carrier of C
product (Carrier CCC) is functional non empty with_common_domain product-like set
the carrier of (T,C,CCC) is non empty set
[: the carrier of C,(product (Carrier CCC)):] is Relation-like non empty set
[y,M] is V15() set
{y,M} is non empty set
{y} is non empty trivial 1 -element set
{{y,M},{y}} is non empty set
p is Element of the carrier of (T,C,CCC)
q is Element of the carrier of (T,C,CCC)
(T,C,CCC) . q is Element of the carrier of T
the mapping of (T,C,CCC) is Relation-like the carrier of (T,C,CCC) -defined the carrier of T -valued Function-like non empty V14( the carrier of (T,C,CCC)) quasi_total Element of bool [: the carrier of (T,C,CCC), the carrier of T:]
[: the carrier of (T,C,CCC), the carrier of T:] is Relation-like non empty set
bool [: the carrier of (T,C,CCC), the carrier of T:] is non empty set
the mapping of (T,C,CCC) . q is Element of the carrier of T
M is Element of the carrier of C
N is Relation-like the carrier of C -defined Function-like Carrier CCC -compatible non empty V14( the carrier of C) Element of product (Carrier CCC)
[M,N] is V15() set
{M,N} is non empty set
{M} is non empty trivial 1 -element set
{{M,N},{M}} is non empty set
product CCC is non empty strict transitive directed RelStr
the carrier of (product CCC) is functional non empty set
Y9 is Relation-like Function-like Element of the carrier of (product CCC)
the InternalRel of (T,C,CCC) is Relation-like the carrier of (T,C,CCC) -defined the carrier of (T,C,CCC) -valued Element of bool [: the carrier of (T,C,CCC), the carrier of (T,C,CCC):]
[: the carrier of (T,C,CCC), the carrier of (T,C,CCC):] is Relation-like non empty set
bool [: the carrier of (T,C,CCC), the carrier of (T,C,CCC):] is non empty set
RelStr(# the carrier of (T,C,CCC), the InternalRel of (T,C,CCC) #) is non empty strict RelStr
[:C,(product CCC):] is non empty strict transitive directed RelStr
YY is Element of the carrier of C
[YY,Y9] is V15() Element of the carrier of [:C,(product CCC):]
the carrier of [:C,(product CCC):] is non empty set
{YY,Y9} is non empty set
{YY} is non empty trivial 1 -element set
{{YY,Y9},{YY}} is non empty set
X is Element of the carrier of C
Y is Relation-like Function-like Element of the carrier of (product CCC)
[X,Y] is V15() Element of the carrier of [:C,(product CCC):]
{X,Y} is non empty set
{X} is non empty trivial 1 -element set
{{X,Y},{X}} is non empty set
( the carrier of C,T,CCC,X) is non empty transitive directed NetStr over T
Y9 . X is Element of the carrier of (CCC . X)
CCC . X is non empty RelStr
the carrier of (CCC . X) is non empty set
Y . X is Element of the carrier of (CCC . X)
X is Relation-like Function-like set
J is Relation-like Function-like set
the carrier of ( the carrier of C,T,CCC,X) is non empty set
M . X is set
( the carrier of C,T,CCC,X) . (Y . X) is Element of the carrier of T
the mapping of ( the carrier of C,T,CCC,X) is Relation-like the carrier of ( the carrier of C,T,CCC,X) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C,T,CCC,X)) quasi_total Element of bool [: the carrier of ( the carrier of C,T,CCC,X), the carrier of T:]
[: the carrier of ( the carrier of C,T,CCC,X), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C,T,CCC,X), the carrier of T:] is non empty set
the mapping of ( the carrier of C,T,CCC,X) . (Y . X) is Element of the carrier of T
J is RelStr
the carrier of J is set
X is Element of the carrier of ( the carrier of C,T,CCC,X)
J is Element of the carrier of J
X9 is Element of the carrier of J
T is non empty 1-sorted
(T) is non empty set
the carrier of T is non empty set
[:(T), the carrier of T:] is Relation-like non empty set
T is non empty 1-sorted
C is (T)
(T) is non empty set
the carrier of T is non empty set
[:(T), the carrier of T:] is Relation-like non empty set
bool [:(T), the carrier of T:] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
(T) is non empty set
[:(T), the carrier of T:] is Relation-like non empty set
bool [:(T), the carrier of T:] is non empty set
C is Relation-like (T) -defined the carrier of T -valued Element of bool [:(T), the carrier of T:]
CC is Relation-like (T)
CCC is non empty transitive directed NetStr over T
(T,CCC) is Element of bool the carrier of T
bool the carrier of T is non empty set
C9 is Element of the carrier of T
[CCC,C9] is V15() set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
x is non empty transitive directed NetStr over T
y is Element of the carrier of T
(T,x) is Element of bool the carrier of T
C is Relation-like (T)
CC is Relation-like (T)
CCC is set
C9 is set
[CCC,C9] is V15() set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
[:(T), the carrier of T:] is Relation-like 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
y is non empty transitive strict directed NetStr over T
the carrier of y is non empty set
x is Element of the carrier of T
[y,x] is V15() set
{y,x} is non empty set
{y} is non empty trivial 1 -element set
{{y,x},{y}} is non empty set
(T,y) is Element of bool the carrier of T
bool 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
y is non empty transitive strict directed NetStr over T
the carrier of y is non empty set
x is Element of the carrier of T
[y,x] is V15() set
{y,x} is non empty set
{y} is non empty trivial 1 -element set
{{y,x},{y}} is non empty set
(T,y) is Element of bool the carrier of T
bool the carrier of T is non empty set
T is non empty 1-sorted
T is non empty TopSpace-like TopStruct
(T) is Relation-like (T)
CC is non empty transitive directed (T) (T) NetStr over T
(T) is non empty set
(T,CC) is Element of the carrier of T
the carrier of T is non empty set
[CC,(T,CC)] is V15() set
{CC,(T,CC)} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,(T,CC)},{CC}} is non empty set
(T,CC) is Element of bool the carrier of T
bool the carrier of T is non empty set
CC is non empty transitive directed NetStr over T
(T) is non empty set
the carrier of T is non empty set
CCC is non empty transitive directed (T,CC)
C9 is Element of the carrier of T
[CC,C9] is V15() set
{CC,C9} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,C9},{CC}} is non empty set
[CCC,C9] is V15() set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
(T,CC) is Element of bool the carrier of T
bool the carrier of T is non empty set
(T,CCC) is Element of bool the carrier of T
the carrier of T is non empty set
CC is non empty transitive directed NetStr over T
(T) is non empty set
CCC is Element of the carrier of T
[CC,CCC] is V15() set
{CC,CCC} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,CCC},{CC}} is non empty set
(T,CC) is Element of bool the carrier of T
bool the carrier of T is non empty set
C9 is non empty transitive directed (T,CC)
x is non empty transitive directed (T,C9)
[x,CCC] is V15() set
{x,CCC} is non empty set
{x} is non empty trivial 1 -element set
{{x,CCC},{x}} is non empty set
(T,x) is Element of bool the carrier of T
the carrier of T is non empty set
CC is non empty transitive directed NetStr over T
the carrier of CC is non empty set
CCC is Element of the carrier of T
[CC,CCC] is V15() set
{CC,CCC} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,CCC},{CC}} is non empty set
C9 is Relation-like the carrier of CC -defined Function-like non empty V14( the carrier of CC) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of CC,T)
(T,CC,C9) is non empty transitive strict directed NetStr over T
[(T,CC,C9),CCC] is V15() set
{(T,CC,C9),CCC} is non empty set
{(T,CC,C9)} is non empty trivial 1 -element set
{{(T,CC,C9),CCC},{(T,CC,C9)}} is non empty set
x is Element of the carrier of CC
( the carrier of CC,T,C9,x) is non empty transitive directed NetStr over T
CC . x is Element of the carrier of T
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 CC . x is Element of the carrier of T
[( the carrier of CC,T,C9,x),(CC . x)] is V15() set
{( the carrier of CC,T,C9,x),(CC . x)} is non empty set
{( the carrier of CC,T,C9,x)} is non empty trivial 1 -element set
{{( the carrier of CC,T,C9,x),(CC . x)},{( the carrier of CC,T,C9,x)}} is non empty set
(T,( the carrier of CC,T,C9,x)) is Element of bool the carrier of T
bool the carrier of T is non empty set
(T) is non empty set
(T,CC) is Element of bool the carrier of T
(T,(T,CC,C9)) is Element of bool the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
bool the carrier of T is non empty set
C is Relation-like (T)
{ b₁ where b₁ is Element of bool the carrier of T : for b₂ being Element of the carrier of T holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over T holds
( not [b₃,b₂] in C or b₃ is_eventually_in b₁ ) ) } is set
bool (bool the carrier of T) is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : S₁[b₁] } is set
CC is Element of bool (bool the carrier of T)
TopStruct(# the carrier of T,CC #) is strict TopStruct
the carrier of TopStruct(# the carrier of T,CC #) is set
the topology of TopStruct(# the carrier of T,CC #) is Element of bool (bool the carrier of TopStruct(# the carrier of T,CC #))
bool the carrier of TopStruct(# the carrier of T,CC #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of T,CC #)) is non empty set
CC is strict TopStruct
the carrier of CC is set
the topology of CC is Element of bool (bool the carrier of CC)
bool the carrier of CC is non empty set
bool (bool the carrier of CC) is non empty set
CCC is strict TopStruct
the carrier of CCC is set
the topology of CCC is Element of bool (bool the carrier of CCC)
bool the carrier of CCC is non empty set
bool (bool the carrier of CCC) is non empty set
T is non empty 1-sorted
C is Relation-like (T)
(T,C) is strict TopStruct
the carrier of (T,C) is set
the carrier of T is non empty set
T is non empty 1-sorted
C is Relation-like (T)
(T,C) is non empty strict TopStruct
the topology of (T,C) is Element of bool (bool the carrier of (T,C))
the carrier of (T,C) is non empty set
bool the carrier of (T,C) is non empty set
bool (bool the carrier of (T,C)) is non empty set
the carrier of T is non empty set
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : for b₂ being Element of the carrier of T holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over T holds
( not [b₃,b₂] in C or b₃ is_eventually_in b₁ ) ) } is set
[#] (T,C) is non empty non proper dense Element of bool the carrier of (T,C)
CCC is Element of bool the carrier of T
C9 is Element of the carrier of T
x is non empty transitive directed NetStr over T
[x,C9] is V15() set
{x,C9} is non empty set
{x} is non empty trivial 1 -element set
{{x,C9},{x}} is non empty set
C9 is Element of bool (bool the carrier of (T,C))
union C9 is Element of bool the carrier of (T,C)
y is Element of the carrier of T
x is Element of bool the carrier of T
M is set
p is non empty transitive directed NetStr over T
[p,y] is V15() set
{p,y} is non empty set
{p} is non empty trivial 1 -element set
{{p,y},{p}} is non empty set
q is Element of bool the carrier of T
C9 is Element of bool the carrier of (T,C)
x is Element of bool the carrier of (T,C)
C9 /\ x is Element of bool the carrier of (T,C)
y is Element of bool the carrier of T
p is Element of bool the carrier of T
q is Element of the carrier of T
M is Element of bool the carrier of T
M is non empty transitive directed NetStr over T
[M,q] is V15() set
{M,q} is non empty set
{M} is non empty trivial 1 -element set
{{M,q},{M}} is non empty set
the carrier of M is non empty set
N is Element of the carrier of M
Y is Element of the carrier of M
Y9 is Element of the carrier of M
YY is Element of the carrier of M
M . YY is Element of the carrier of T
the mapping of M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
[: the carrier of M, the carrier of T:] is Relation-like non empty set
bool [: the carrier of M, the carrier of T:] is non empty set
the mapping of M . YY is Element of the carrier of T
T is non empty 1-sorted
C is Relation-like (T)
(T,C) is non empty strict TopSpace-like TopStruct
((T,C)) is Relation-like ((T,C)) ((T,C)) ((T,C)) ((T,C)) ((T,C))
CCC is set
C9 is set
[CCC,C9] is V15() set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
(T) is non empty set
the carrier of T is non empty set
[:(T), the carrier of T:] is Relation-like non empty set
x is Element of (T)
y is Element of the carrier of T
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty trivial 1 -element set
{{x,y},{x}} is non empty set
the carrier of (T,C) 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
q is non empty transitive strict directed NetStr over T
the carrier of q is non empty set
p is non empty transitive directed NetStr over T
the topology of (T,C) is Element of bool (bool the carrier of (T,C))
bool the carrier of (T,C) is non empty set
bool (bool the carrier of (T,C)) is non empty set
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : for b₂ being Element of the carrier of T holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over T holds
( not [b₃,b₂] in C or b₃ is_eventually_in b₁ ) ) } is set
M is Element of the carrier of (T,C)
M is a_neighborhood of M
Int M is open Element of bool the carrier of (T,C)
N is Element of bool the carrier of T
the carrier of p is non empty set
N is Element of the carrier of p
q is non empty transitive directed NetStr over (T,C)
the carrier of q is non empty set
Y is Element of the carrier of q
Y9 is Element of the carrier of q
YY is Element of the carrier of p
p . YY is Element of the carrier of T
the mapping of p is Relation-like the carrier of p -defined the carrier of T -valued Function-like non empty V14( the carrier of p) quasi_total Element of bool [: the carrier of p, the carrier of T:]
[: the carrier of p, the carrier of T:] is Relation-like non empty set
bool [: the carrier of p, the carrier of T:] is non empty set
the mapping of p . YY is Element of the carrier of T
q . Y9 is Element of the carrier of (T,C)
the mapping of q is Relation-like the carrier of q -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of q) quasi_total Element of bool [: the carrier of q, the carrier of (T,C):]
[: the carrier of q, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of q, the carrier of (T,C):] is non empty set
the mapping of q . Y9 is Element of the carrier of (T,C)
((T,C),q) is Element of bool the carrier of (T,C)
((T,C)) is non empty set
T is non empty 1-sorted
T is non empty 1-sorted
(T) is non empty set
the carrier of T is non empty set
[:(T), the carrier of T:] is Relation-like non empty set
C is Relation-like (T)
CC is non empty transitive directed (T) NetStr over T
(T,CC) is Element of the carrier of T
[CC,(T,CC)] is V15() set
{CC,(T,CC)} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,(T,CC)},{CC}} is non empty set
CC is non empty transitive directed NetStr over T
CCC is non empty transitive directed (T,CC)
C9 is Element of the carrier of T
[CC,C9] is V15() set
{CC,C9} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,C9},{CC}} is non empty set
[CCC,C9] is V15() set
{CCC,C9} is non empty set
{CCC} is non empty trivial 1 -element set
{{CCC,C9},{CCC}} is non empty set
CC is non empty transitive directed NetStr over T
CCC is Element of the carrier of T
[CC,CCC] is V15() set
{CC,CCC} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,CCC},{CC}} is non empty set
CC is non empty transitive directed NetStr over T
the carrier of CC is non empty set
CCC is Element of the carrier of T
[CC,CCC] is V15() set
{CC,CCC} is non empty set
{CC} is non empty trivial 1 -element set
{{CC,CCC},{CC}} is non empty set
C9 is Relation-like the carrier of CC -defined Function-like non empty V14( the carrier of CC) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of CC,T)
(T,CC,C9) is non empty transitive strict directed NetStr over T
[(T,CC,C9),CCC] is V15() set
{(T,CC,C9),CCC} is non empty set
{(T,CC,C9)} is non empty trivial 1 -element set
{{(T,CC,C9),CCC},{(T,CC,C9)}} is non empty set
x is Element of the carrier of CC
( the carrier of CC,T,C9,x) is non empty transitive directed NetStr over T
CC . x is Element of the carrier of T
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 CC . x is Element of the carrier of T
[( the carrier of CC,T,C9,x),(CC . x)] is V15() set
{( the carrier of CC,T,C9,x),(CC . x)} is non empty set
{( the carrier of CC,T,C9,x)} is non empty trivial 1 -element set
{{( the carrier of CC,T,C9,x),(CC . x)},{( the carrier of CC,T,C9,x)}} is non empty set
T is non empty 1-sorted
C is Relation-like (T)
C is Relation-like (T)
T is non empty 1-sorted
the carrier of T is non empty set
C is Relation-like (T) (T) (T) (T) (T) (T)
(T,C) is non empty strict TopSpace-like TopStruct
the carrier of (T,C) is non empty set
bool the carrier of (T,C) is non empty set
CC is Element of bool the carrier of (T,C)
the topology of (T,C) is Element of bool (bool the carrier of (T,C))
bool (bool the carrier of (T,C)) is non empty set
bool the carrier of T is non empty set
{ b₁ where b₁ is Element of bool the carrier of T : for b₂ being Element of the carrier of T holds
( not b₂ in b₁ or for b₃ being non empty transitive directed NetStr over T holds
( not [b₃,b₂] in C or b₃ is_eventually_in b₁ ) ) } is set
CCC is Element of the carrier of T
C9 is non empty transitive directed NetStr over T
[C9,CCC] is V15() set
{C9,CCC} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,CCC},{C9}} is non empty set
x is Element of the carrier of T
y is non empty transitive directed NetStr over T
[y,x] is V15() set
{y,x} is non empty set
{y} is non empty trivial 1 -element set
{{y,x},{y}} is non empty set
M is Element of bool the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
C is Relation-like (T) (T) (T) (T) (T) (T)
(T,C) is non empty strict TopSpace-like TopStruct
the carrier of (T,C) is non empty set
bool the carrier of (T,C) is non empty set
CC is Element of bool the carrier of (T,C)
CC ` is Element of bool the carrier of (T,C)
the carrier of (T,C) \ CC is set
x is non empty transitive directed NetStr over T
C9 is Element of the carrier of T
[x,C9] is V15() set
{x,C9} is non empty set
{x} is non empty trivial 1 -element set
{{x,C9},{x}} is non empty set
[#] (T,C) is non empty non proper open dense non boundary Element of bool the carrier of (T,C)
([#] (T,C)) \ CC is Element of bool the carrier of (T,C)
C9 is Element of the carrier of T
x is non empty transitive directed NetStr over T
[x,C9] is V15() set
{x,C9} is non empty set
{x} is non empty trivial 1 -element set
{{x,C9},{x}} is non empty set
T is non empty 1-sorted
C is Relation-like (T) (T) (T) (T) (T) (T)
(T,C) is non empty strict TopSpace-like TopStruct
the carrier of (T,C) is non empty set
bool the carrier of (T,C) is non empty set
CC is Element of bool the carrier of (T,C)
Cl CC is closed Element of bool the carrier of (T,C)
CCC is Element of the carrier of (T,C)
{ b₁ where b₁ is Element of the carrier of (T,C) : S₁[b₁] } is set
the carrier of T is non empty set
y is Element of bool the carrier of (T,C)
M is Element of the carrier of T
q is non empty transitive directed NetStr over T
[q,M] is V15() set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
(T) is non empty set
[:(T), the carrier of T:] is Relation-like 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
(T,q,y) is transitive strict (T,q) (T,q)
M is non empty transitive directed (T,q)
the carrier of M is non empty set
N is Element of the carrier of M
the carrier of q is non empty set
the mapping of q is Relation-like the carrier of q -defined the carrier of T -valued Function-like non empty V14( the carrier of q) quasi_total Element of bool [: the carrier of q, the carrier of T:]
[: the carrier of q, the carrier of T:] is Relation-like non empty set
bool [: the carrier of q, the carrier of T:] is non empty set
the mapping of q " y is Element of bool the carrier of q
bool the carrier of q is non empty set
the mapping of q . N is set
the mapping of M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
[: the carrier of M, the carrier of T:] is Relation-like non empty set
bool [: the carrier of M, the carrier of T:] is non empty set
the mapping of q | the carrier of M is Relation-like the carrier of M -defined the carrier of q -defined the carrier of T -valued Function-like Element of bool [: the carrier of q, the carrier of T:]
the mapping of M . N is Element of the carrier of T
M . N is Element of the carrier of T
Y is Element of the carrier of (T,C)
Y9 is non empty transitive directed NetStr over (T,C)
[Y9,Y] is V15() set
{Y9,Y} is non empty set
{Y9} is non empty trivial 1 -element set
{{Y9,Y},{Y9}} is non empty set
the mapping of Y9 is Relation-like the carrier of Y9 -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of Y9) quasi_total Element of bool [: the carrier of Y9, the carrier of (T,C):]
the carrier of Y9 is non empty set
[: the carrier of Y9, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of Y9, the carrier of (T,C):] is non empty set
rng the mapping of Y9 is non empty Element of bool the carrier of (T,C)
((T,C),Y9) is Element of bool the carrier of (T,C)
Y9 is non empty transitive directed NetStr over (T,C)
[Y9,Y] is V15() set
{Y9,Y} is non empty set
{Y9} is non empty trivial 1 -element set
{{Y9,Y},{Y9}} is non empty set
the mapping of Y9 is Relation-like the carrier of Y9 -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of Y9) quasi_total Element of bool [: the carrier of Y9, the carrier of (T,C):]
the carrier of Y9 is non empty set
[: the carrier of Y9, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of Y9, the carrier of (T,C):] is non empty set
rng the mapping of Y9 is non empty Element of bool the carrier of (T,C)
((T,C),Y9) is Element of bool the carrier of (T,C)
YY is set
X is set
[X,(M . N)] is V15() set
{X,(M . N)} is non empty set
{X} is non empty trivial 1 -element set
{{X,(M . N)},{X}} is non empty set
X is non empty transitive directed NetStr over T
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 is non empty set
[: 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
rng the mapping of X is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
N is Relation-like the carrier of M -defined Function-like non empty V14( the carrier of M) set
Y is set
N . Y is set
Y9 is non empty transitive directed NetStr over T
the mapping of Y9 is Relation-like the carrier of Y9 -defined the carrier of T -valued Function-like non empty V14( the carrier of Y9) quasi_total Element of bool [: the carrier of Y9, the carrier of T:]
the carrier of Y9 is non empty set
[: the carrier of Y9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of Y9, the carrier of T:] is non empty set
rng the mapping of Y9 is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
Y is Relation-like the carrier of M -defined Function-like non empty V14( the carrier of M) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of M,T)
{ (rng the mapping of ( the carrier of M,T,Y,b₁)) where b₁ is Element of the carrier of M : verum } is set
YY is Element of the carrier of M
( the carrier of M,T,Y,YY) is non empty transitive directed NetStr over T
M . YY is Element of the carrier of T
the mapping of M . YY is Element of the carrier of T
[( the carrier of M,T,Y,YY),(M . YY)] is V15() set
{( the carrier of M,T,Y,YY),(M . YY)} is non empty set
{( the carrier of M,T,Y,YY)} is non empty trivial 1 -element set
{{( the carrier of M,T,Y,YY),(M . YY)},{( the carrier of M,T,Y,YY)}} is non empty set
the mapping of ( the carrier of M,T,Y,YY) is Relation-like the carrier of ( the carrier of M,T,Y,YY) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of M,T,Y,YY)) quasi_total Element of bool [: the carrier of ( the carrier of M,T,Y,YY), the carrier of T:]
the carrier of ( the carrier of M,T,Y,YY) is non empty set
[: the carrier of ( the carrier of M,T,Y,YY), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of M,T,Y,YY), the carrier of T:] is non empty set
rng the mapping of ( the carrier of M,T,Y,YY) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
X is non empty transitive directed NetStr over T
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 is non empty set
[: 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
rng the mapping of X is non empty Element of bool the carrier of T
YY is set
X is Element of the carrier of M
( the carrier of M,T,Y,X) is non empty transitive directed NetStr over T
the mapping of ( the carrier of M,T,Y,X) is Relation-like the carrier of ( the carrier of M,T,Y,X) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of M,T,Y,X)) quasi_total Element of bool [: the carrier of ( the carrier of M,T,Y,X), the carrier of T:]
the carrier of ( the carrier of M,T,Y,X) is non empty set
[: the carrier of ( the carrier of M,T,Y,X), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of M,T,Y,X), the carrier of T:] is non empty set
rng the mapping of ( the carrier of M,T,Y,X) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
union { (rng the mapping of ( the carrier of M,T,Y,b₁)) where b₁ is Element of the carrier of M : verum } is set
(T,M,Y) is non empty transitive strict directed NetStr over T
YY is non empty transitive directed NetStr over (T,C)
the mapping of YY is Relation-like the carrier of YY -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of YY) quasi_total Element of bool [: the carrier of YY, the carrier of (T,C):]
the carrier of YY is non empty set
[: the carrier of YY, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of YY, the carrier of (T,C):] is non empty set
rng the mapping of YY is non empty Element of bool the carrier of (T,C)
X is non empty transitive strict directed NetStr over T
the carrier of X is non empty set
[M,M] is V15() set
{M,M} is non empty set
{M} is non empty trivial 1 -element set
{{M,M},{M}} is non empty set
[YY,M] is V15() set
{YY,M} is non empty set
{YY} is non empty trivial 1 -element set
{{YY,M},{YY}} is non empty set
((T,C)) is Relation-like ((T,C)) ((T,C)) ((T,C)) ((T,C)) ((T,C)) ((T,C))
p is Element of the carrier of (T,C)
((T,C),YY) is Element of bool the carrier of (T,C)
[:{{}},{{}}:] 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
M is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]
RelStr(# {{}},M #) is non empty trivial V63() 1 -element strict RelStr
the carrier of RelStr(# {{}},M #) is non empty trivial V48() 1 -element countable set
q is Element of the carrier of RelStr(# {{}},M #)
M is Element of the carrier of RelStr(# {{}},M #)
[q,M] is V15() Element of the carrier of [:RelStr(# {{}},M #),RelStr(# {{}},M #):]
[:RelStr(# {{}},M #),RelStr(# {{}},M #):] is non empty strict RelStr
the carrier of [:RelStr(# {{}},M #),RelStr(# {{}},M #):] is non empty set
{q,M} is non empty set
{q} is non empty trivial 1 -element set
{{q,M},{q}} is non empty set
q is Element of the carrier of RelStr(# {{}},M #)
M is Element of the carrier of RelStr(# {{}},M #)
N is Element of the carrier of RelStr(# {{}},M #)
q is Element of the carrier of RelStr(# {{}},M #)
M is Element of the carrier of RelStr(# {{}},M #)
M 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
q is non empty transitive directed RelStr
Y is Element of the carrier of (T,C)
(q,(T,C),Y) is non empty transitive strict directed ((T,C)) ((T,C)) NetStr over (T,C)
the carrier of (q,(T,C),Y) is non empty set
the mapping of (q,(T,C),Y) is Relation-like the carrier of (q,(T,C),Y) -defined the carrier of (T,C) -valued Function-like constant non empty V14( the carrier of (q,(T,C),Y)) quasi_total Element of bool [: the carrier of (q,(T,C),Y), the carrier of (T,C):]
[: the carrier of (q,(T,C),Y), the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of (q,(T,C),Y), the carrier of (T,C):] is non empty set
the carrier of (q,(T,C),Y) --> Y is Relation-like the carrier of (q,(T,C),Y) -defined the carrier of (T,C) -valued Function-like constant non empty V14( the carrier of (q,(T,C),Y)) quasi_total Element of bool [: the carrier of (q,(T,C),Y), the carrier of (T,C):]
rng the mapping of (q,(T,C),Y) is non empty trivial 1 -element Element of bool the carrier of (T,C)
{Y} is non empty trivial 1 -element set
the carrier of q is non empty set
((T,C),(q,(T,C),Y)) is Element of the carrier of (T,C)
YY is non empty transitive strict directed (T) NetStr over T
the mapping of YY is Relation-like the carrier of YY -defined the carrier of T -valued Function-like constant non empty V14( the carrier of YY) quasi_total Element of bool [: the carrier of YY, the carrier of T:]
the carrier of YY is non empty set
[: the carrier of YY, the carrier of T:] is Relation-like non empty set
bool [: the carrier of YY, the carrier of T:] is non empty set
the_value_of the mapping of YY is set
(T,YY) is Element of the carrier of T
the InternalRel of (q,(T,C),Y) is Relation-like the carrier of (q,(T,C),Y) -defined the carrier of (q,(T,C),Y) -valued Element of bool [: the carrier of (q,(T,C),Y), the carrier of (q,(T,C),Y):]
[: the carrier of (q,(T,C),Y), the carrier of (q,(T,C),Y):] is Relation-like non empty set
bool [: the carrier of (q,(T,C),Y), the carrier of (q,(T,C),Y):] is non empty set
RelStr(# the carrier of (q,(T,C),Y), the InternalRel of (q,(T,C),Y) #) is non empty strict RelStr
the InternalRel of q is Relation-like the carrier of q -defined the carrier of q -valued Element of bool [: the carrier of q, the carrier of q:]
[: the carrier of q, the carrier of q:] is Relation-like non empty set
bool [: the carrier of q, the carrier of q:] is non empty set
RelStr(# the carrier of q, the InternalRel of q #) is non empty strict RelStr
(T) is non empty set
[YY,Y] is V15() set
{YY,Y} is non empty set
{YY} is non empty trivial 1 -element set
{{YY,Y},{YY}} is non empty set
((T,C),(q,(T,C),Y)) is Element of bool the carrier of (T,C)
M is Element of the carrier of (T,C)
p is non empty transitive directed NetStr over (T,C)
[p,M] is V15() set
{p,M} is non empty set
{p} is non empty trivial 1 -element set
{{p,M},{p}} is non empty set
the mapping of p is Relation-like the carrier of p -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of p) quasi_total Element of bool [: the carrier of p, the carrier of (T,C):]
the carrier of p is non empty set
[: the carrier of p, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of p, the carrier of (T,C):] is non empty set
rng the mapping of p is non empty Element of bool the carrier of (T,C)
((T,C),p) is Element of bool the carrier of (T,C)
T is non empty 1-sorted
C is Relation-like (T)
(T,C) is non empty strict TopSpace-like TopStruct
((T,C)) is Relation-like ((T,C)) ((T,C)) ((T,C)) ((T,C)) ((T,C)) ((T,C))
the carrier of (T,C) is non empty set
the carrier of T is non empty set
C9 is non empty transitive directed NetStr over T
x is non empty transitive directed NetStr over (T,C)
y is non empty transitive directed ((T,C),x)
the carrier of y is non empty set
the carrier of x is non empty set
[: the carrier of y, the carrier of x:] is Relation-like non empty set
bool [: the carrier of y, the carrier of x:] is non empty set
the mapping of y is Relation-like the carrier of y -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of (T,C):]
[: the carrier of y, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of y, the carrier of (T,C):] is non empty set
the mapping of x is Relation-like the carrier of x -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of (T,C):]
[: the carrier of x, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of x, the carrier of (T,C):] is non empty set
p is Relation-like the carrier of y -defined the carrier of x -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of x:]
the mapping of x * p is Relation-like the carrier of y -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of (T,C):]
M is non empty transitive directed NetStr over T
the carrier of M is non empty set
the carrier of C9 is non empty set
[: the carrier of M, the carrier of C9:] is Relation-like non empty set
bool [: the carrier of M, the carrier of C9:] is non empty set
the mapping of M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
[: the carrier of M, the carrier of T:] is Relation-like non empty set
bool [: the carrier of M, the carrier of T:] is non empty set
q is Relation-like the carrier of M -defined the carrier of C9 -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of C9:]
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like non empty V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of T:]
[: the carrier of C9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C9, the carrier of T:] is non empty set
the mapping of C9 * q is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of T:]
C9 is non empty transitive directed NetStr over T
x is non empty transitive directed NetStr over (T,C)
y is non empty transitive directed (T,C9)
the carrier of y is non empty set
the carrier of C9 is non empty set
[: the carrier of y, the carrier of C9:] is Relation-like non empty set
bool [: the carrier of y, the carrier of C9:] is non empty set
the mapping of y is Relation-like the carrier of y -defined the carrier of T -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of T:]
[: the carrier of y, the carrier of T:] is Relation-like non empty set
bool [: the carrier of y, the carrier of T:] is non empty set
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like non empty V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of T:]
[: the carrier of C9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C9, the carrier of T:] is non empty set
p is Relation-like the carrier of y -defined the carrier of C9 -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of C9:]
the mapping of C9 * p is Relation-like the carrier of y -defined the carrier of T -valued Function-like non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of T:]
M is non empty transitive directed NetStr over (T,C)
the carrier of M is non empty set
the carrier of x is non empty set
[: the carrier of M, the carrier of x:] is Relation-like non empty set
bool [: the carrier of M, the carrier of x:] is non empty set
the mapping of M is Relation-like the carrier of M -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of (T,C):]
[: the carrier of M, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of M, the carrier of (T,C):] is non empty set
q is Relation-like the carrier of M -defined the carrier of x -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of x:]
the mapping of x is Relation-like the carrier of x -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of (T,C):]
[: the carrier of x, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of x, the carrier of (T,C):] is non empty set
the mapping of x * q is Relation-like the carrier of M -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of (T,C):]
C9 is non empty transitive directed NetStr over T
C9 is non empty transitive directed NetStr over T
(T) is non empty set
x is non empty transitive directed (T,C9)
y is non empty transitive directed NetStr over (T,C)
M is non empty transitive directed ((T,C),y)
((T,C)) is non empty set
p is Element of the carrier of T
[C9,p] is V15() set
{C9,p} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,p},{C9}} is non empty set
[x,p] is V15() set
{x,p} is non empty set
{x} is non empty trivial 1 -element set
{{x,p},{x}} is non empty set
q is Element of the carrier of (T,C)
[y,q] is V15() set
{y,q} is non empty set
{y} is non empty trivial 1 -element set
{{y,q},{y}} is non empty set
C9 is non empty transitive directed NetStr over T
the carrier of C9 is non empty set
x is Element of the carrier of T
[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
p is Relation-like the carrier of C9 -defined Function-like non empty V14( the carrier of C9) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of C9,T)
(T,C9,p) is non empty transitive strict directed NetStr over T
[(T,C9,p),x] is V15() set
{(T,C9,p),x} is non empty set
{(T,C9,p)} is non empty trivial 1 -element set
{{(T,C9,p),x},{(T,C9,p)}} is non empty set
M is non empty transitive directed NetStr over (T,C)
the carrier of M is non empty set
q is Relation-like the carrier of M -defined Function-like non empty V14( the carrier of M) set
M is set
proj2 q is non empty set
N is Element of the carrier of M
Y is Element of the carrier of C9
C9 . Y is Element of the carrier of T
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like non empty V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of T:]
[: the carrier of C9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C9, the carrier of T:] is non empty set
the mapping of C9 . Y is Element of the carrier of T
M . N is Element of the carrier of (T,C)
the mapping of M is Relation-like the carrier of M -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of M) quasi_total Element of bool [: the carrier of M, the carrier of (T,C):]
[: the carrier of M, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of M, the carrier of (T,C):] is non empty set
the mapping of M . N is Element of the carrier of (T,C)
M is Relation-like the carrier of M -defined Function-like non empty V14( the carrier of M) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of M,(T,C))
( the carrier of M,(T,C),M,N) is non empty transitive directed NetStr over (T,C)
[( the carrier of M,(T,C),M,N),(M . N)] is V15() set
{( the carrier of M,(T,C),M,N),(M . N)} is non empty set
{( the carrier of M,(T,C),M,N)} is non empty trivial 1 -element set
{{( the carrier of M,(T,C),M,N),(M . N)},{( the carrier of M,(T,C),M,N)}} is non empty set
((T,C),M,M) is non empty transitive strict directed NetStr over (T,C)
y is Element of the carrier of (T,C)
[((T,C),M,M),y] is V15() set
{((T,C),M,M),y} is non empty set
{((T,C),M,M)} is non empty trivial 1 -element set
{{((T,C),M,M),y},{((T,C),M,M)}} is non empty set
the carrier of ((T,C),M,M) is non empty set
the InternalRel of ((T,C),M,M) is Relation-like the carrier of ((T,C),M,M) -defined the carrier of ((T,C),M,M) -valued Element of bool [: the carrier of ((T,C),M,M), the carrier of ((T,C),M,M):]
[: the carrier of ((T,C),M,M), the carrier of ((T,C),M,M):] is Relation-like non empty set
bool [: the carrier of ((T,C),M,M), the carrier of ((T,C),M,M):] is non empty set
RelStr(# the carrier of ((T,C),M,M), the InternalRel of ((T,C),M,M) #) is non empty strict RelStr
product p is non empty strict transitive directed RelStr
[:C9,(product p):] is non empty strict transitive directed RelStr
the carrier of (T,C9,p) is non empty set
the InternalRel of (T,C9,p) is Relation-like the carrier of (T,C9,p) -defined the carrier of (T,C9,p) -valued Element of bool [: the carrier of (T,C9,p), the carrier of (T,C9,p):]
[: the carrier of (T,C9,p), the carrier of (T,C9,p):] is Relation-like non empty set
bool [: the carrier of (T,C9,p), the carrier of (T,C9,p):] is non empty set
RelStr(# the carrier of (T,C9,p), the InternalRel of (T,C9,p) #) is non empty strict RelStr
N is set
the mapping of ((T,C),M,M) is Relation-like the carrier of ((T,C),M,M) -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of ((T,C),M,M)) quasi_total Element of bool [: the carrier of ((T,C),M,M), the carrier of (T,C):]
[: the carrier of ((T,C),M,M), the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of ((T,C),M,M), the carrier of (T,C):] is non empty set
dom the mapping of ((T,C),M,M) is non empty Element of bool the carrier of ((T,C),M,M)
bool the carrier of ((T,C),M,M) is non empty set
Carrier M is Relation-like non-empty non empty-yielding the carrier of M -defined Function-like non empty V14( the carrier of M) set
product (Carrier M) is functional non empty with_common_domain product-like set
[: the carrier of M,(product (Carrier M)):] is Relation-like non empty set
Y is Element of the carrier of ((T,C),M,M)
Y9 is Element of the carrier of M
YY is Relation-like the carrier of M -defined Function-like Carrier M -compatible non empty V14( the carrier of M) Element of product (Carrier M)
[Y9,YY] is V15() set
{Y9,YY} is non empty set
{Y9} is non empty trivial 1 -element set
{{Y9,YY},{Y9}} is non empty set
product M is non empty strict transitive directed RelStr
the carrier of (product M) is functional non empty set
X is Relation-like Function-like Element of the carrier of (product M)
Carrier p is Relation-like non-empty non empty-yielding the carrier of C9 -defined Function-like non empty V14( the carrier of C9) set
product (Carrier p) is functional non empty with_common_domain product-like set
[: the carrier of C9,(product (Carrier p)):] is Relation-like non empty set
X is Element of the carrier of C9
[X,X] is V15() Element of the carrier of [:C9,(product M):]
[:C9,(product M):] is non empty strict transitive directed RelStr
the carrier of [:C9,(product M):] is non empty set
{X,X} is non empty set
{X} is non empty trivial 1 -element set
{{X,X},{X}} is non empty set
the mapping of ((T,C),M,M) . N is set
((T,C),M,M) . Y is Element of the carrier of (T,C)
the mapping of ((T,C),M,M) . Y is Element of the carrier of (T,C)
M . Y9 is non empty RelStr
the carrier of (M . Y9) is non empty set
( the carrier of M,(T,C),M,Y9) is non empty transitive directed NetStr over (T,C)
the mapping of ( the carrier of M,(T,C),M,Y9) is Relation-like the carrier of ( the carrier of M,(T,C),M,Y9) -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of ( the carrier of M,(T,C),M,Y9)) quasi_total Element of bool [: the carrier of ( the carrier of M,(T,C),M,Y9), the carrier of (T,C):]
the carrier of ( the carrier of M,(T,C),M,Y9) is non empty set
[: the carrier of ( the carrier of M,(T,C),M,Y9), the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of ( the carrier of M,(T,C),M,Y9), the carrier of (T,C):] is non empty set
X . Y9 is Element of the carrier of (M . Y9)
the mapping of ( the carrier of M,(T,C),M,Y9) . (X . Y9) is Element of the carrier of (T,C)
( the carrier of C9,T,p,X) is non empty transitive directed NetStr over T
the mapping of ( the carrier of C9,T,p,X) is Relation-like the carrier of ( the carrier of C9,T,p,X) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of C9,T,p,X)) quasi_total Element of bool [: the carrier of ( the carrier of C9,T,p,X), the carrier of T:]
the carrier of ( the carrier of C9,T,p,X) is non empty set
[: the carrier of ( the carrier of C9,T,p,X), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of C9,T,p,X), the carrier of T:] is non empty set
X . X is set
the mapping of ( the carrier of C9,T,p,X) . (X . X) is set
J is Element of the carrier of (T,C9,p)
(T,C9,p) . J is Element of the carrier of T
the mapping of (T,C9,p) is Relation-like the carrier of (T,C9,p) -defined the carrier of T -valued Function-like non empty V14( the carrier of (T,C9,p)) quasi_total Element of bool [: the carrier of (T,C9,p), the carrier of T:]
[: the carrier of (T,C9,p), the carrier of T:] is Relation-like non empty set
bool [: the carrier of (T,C9,p), the carrier of T:] is non empty set
the mapping of (T,C9,p) . J is Element of the carrier of T
the mapping of (T,C9,p) . N is set
dom the mapping of (T,C9,p) is non empty Element of bool the carrier of (T,C9,p)
bool the carrier of (T,C9,p) is non empty set
C9 is non empty transitive directed NetStr over T
(T) is non empty set
x is Element of the carrier of T
[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
M is non empty transitive directed NetStr over (T,C)
((T,C)) is non empty set
y is Element of the carrier of (T,C)
p is non empty transitive directed ((T,C),M)
q is non empty transitive directed (T,C9)
M is non empty transitive directed (T,q)
[M,x] is V15() set
{M,x} is non empty set
{M} is non empty trivial 1 -element set
{{M,x},{M}} is non empty set
N is non empty transitive directed ((T,C),p)
[N,y] is V15() set
{N,y} is non empty set
{N} is non empty trivial 1 -element set
{{N,y},{N}} is non empty set
C9 is non empty transitive directed (T) NetStr over T
(T) is non empty set
(T,C9) is Element of the carrier of T
[C9,(T,C9)] is V15() set
{C9,(T,C9)} is non empty set
{C9} is non empty trivial 1 -element set
{{C9,(T,C9)},{C9}} is non empty set
the mapping of C9 is Relation-like the carrier of C9 -defined the carrier of T -valued Function-like constant non empty V14( the carrier of C9) quasi_total Element of bool [: the carrier of C9, the carrier of T:]
the carrier of C9 is non empty set
[: the carrier of C9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of C9, the carrier of T:] is non empty set
x is non empty transitive directed NetStr over (T,C)
the mapping of x is Relation-like the carrier of x -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of (T,C):]
the carrier of x is non empty set
[: the carrier of x, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of x, the carrier of (T,C):] is non empty set
y is non empty transitive directed ((T,C)) ((T,C)) NetStr over (T,C)
((T,C)) is non empty set
((T,C),y) is Element of the carrier of (T,C)
the mapping of y is Relation-like the carrier of y -defined the carrier of (T,C) -valued Function-like constant non empty V14( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of (T,C):]
the carrier of y is non empty set
[: the carrier of y, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of y, the carrier of (T,C):] is non empty set
the_value_of the mapping of y is set
the_value_of the mapping of C9 is set
x is set
y is set
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty trivial 1 -element set
{{x,y},{x}} is non empty set
((T,C)) is non empty set
[:((T,C)), the carrier of (T,C):] is Relation-like non empty set
M is Element of ((T,C))
p is Element of the carrier of (T,C)
[M,p] is V15() set
{M,p} is non empty set
{M} is non empty trivial 1 -element set
{{M,p},{M}} is non empty set
( the carrier of (T,C)) is non empty epsilon-transitive subset-closed Tarski universal set
the_transitive-closure_of the carrier of (T,C) is epsilon-transitive set
Tarski-Class (the_transitive-closure_of the carrier of (T,C)) is non empty epsilon-transitive subset-closed Tarski universal set
N is non empty transitive strict directed NetStr over (T,C)
the carrier of N is non empty set
M is non empty transitive directed NetStr over (T,C)
N is non empty transitive directed NetStr over T
(T) is non empty set
q is Element of the carrier of T
Y is non empty transitive directed (T,N)
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of bool [: the carrier of Y, the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is non empty strict RelStr
YY is non empty transitive directed RelStr
(YY,T,q) is non empty transitive strict directed (T) NetStr over T
the carrier of (YY,T,q) is non empty set
the InternalRel of (YY,T,q) is Relation-like the carrier of (YY,T,q) -defined the carrier of (YY,T,q) -valued Element of bool [: the carrier of (YY,T,q), the carrier of (YY,T,q):]
[: the carrier of (YY,T,q), the carrier of (YY,T,q):] is Relation-like non empty set
bool [: the carrier of (YY,T,q), the carrier of (YY,T,q):] is non empty set
RelStr(# the carrier of (YY,T,q), the InternalRel of (YY,T,q) #) is non empty strict RelStr
((T,C),M) is Element of bool the carrier of (T,C)
bool the carrier of (T,C) is non empty set
X is non empty transitive strict directed (T) NetStr over T
the carrier of X is non empty set
J is set
Y9 is non empty transitive directed ((T,C),M)
the carrier of Y9 is non empty set
J is Element of the carrier of Y9
((T,C),Y9) is Element of bool the carrier of (T,C)
{ (Y9 . b₁) where b₁ is Element of the carrier of Y9 : J <= b₁ } is set
X9 is Element of bool the carrier of (T,C)
Cl X9 is closed Element of bool the carrier of (T,C)
C9 is Relation-like (T) (T) (T) (T) (T) (T)
(T,C9) is non empty strict TopSpace-like TopStruct
the carrier of (T,C9) is non empty set
F is non empty transitive directed NetStr over (T,C9)
[F,p] is V15() set
{F,p} is non empty set
{F} is non empty trivial 1 -element set
{{F,p},{F}} is non empty set
the mapping of F is Relation-like the carrier of F -defined the carrier of (T,C9) -valued Function-like non empty V14( the carrier of F) quasi_total Element of bool [: the carrier of F, the carrier of (T,C9):]
the carrier of F is non empty set
[: the carrier of F, the carrier of (T,C9):] is Relation-like non empty set
bool [: the carrier of F, the carrier of (T,C9):] is non empty set
rng the mapping of F is non empty Element of bool the carrier of (T,C9)
bool the carrier of (T,C9) is non empty set
((T,C9),F) is Element of bool the carrier of (T,C9)
h is non empty transitive directed NetStr over T
X9 is Element of the carrier of Y
{ (Y . b₁) where b₁ is Element of the carrier of Y : X9 <= b₁ } is set
[h,p] is V15() set
{h,p} is non empty set
{h} is non empty trivial 1 -element set
{{h,p},{h}} is non empty set
the mapping of h is Relation-like the carrier of h -defined the carrier of T -valued Function-like non empty V14( the carrier of h) quasi_total Element of bool [: the carrier of h, the carrier of T:]
the carrier of h is non empty set
[: the carrier of h, the carrier of T:] is Relation-like non empty set
bool [: the carrier of h, the carrier of T:] is non empty set
rng the mapping of h is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
g is set
B is Element of the carrier of Y9
Y9 . B is Element of the carrier of (T,C)
the mapping of Y9 is Relation-like the carrier of Y9 -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of Y9) quasi_total Element of bool [: the carrier of Y9, the carrier of (T,C):]
[: the carrier of Y9, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of Y9, the carrier of (T,C):] is non empty set
the mapping of Y9 . B is Element of the carrier of (T,C)
B is Element of the carrier of Y
Y . B is Element of the carrier of T
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V14( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of T:]
[: the carrier of Y, the carrier of T:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of T:] is non empty set
the mapping of Y . B is Element of the carrier of T
J is Relation-like the carrier of X -defined Function-like non empty V14( the carrier of X) set
J is set
J . J is set
X9 is Element of the carrier of Y
X9 is non empty transitive directed NetStr over T
[X9,p] is V15() set
{X9,p} is non empty set
{X9} is non empty trivial 1 -element set
{{X9,p},{X9}} is non empty set
the mapping of X9 is Relation-like the carrier of X9 -defined the carrier of T -valued Function-like non empty V14( the carrier of X9) quasi_total Element of bool [: the carrier of X9, the carrier of T:]
the carrier of X9 is non empty set
[: the carrier of X9, the carrier of T:] is Relation-like non empty set
bool [: the carrier of X9, the carrier of T:] is non empty set
rng the mapping of X9 is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
{ (Y . b₁) where b₁ is Element of the carrier of Y : X9 <= b₁ } is set
X9 is non empty transitive directed NetStr over (T,C)
the mapping of X9 is Relation-like the carrier of X9 -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of X9) quasi_total Element of bool [: the carrier of X9, the carrier of (T,C):]
the carrier of X9 is non empty set
[: the carrier of X9, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of X9, the carrier of (T,C):] is non empty set
J is Relation-like the carrier of X -defined Function-like non empty V14( the carrier of X) 1-sorted-yielding RelStr-yielding non-Empty ( the carrier of X,T)
X9 is Element of the carrier of X
( the carrier of X,T,J,X9) is non empty transitive directed NetStr over T
X . X9 is Element of the carrier of T
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like constant 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
the mapping of X . X9 is Element of the carrier of T
[( the carrier of X,T,J,X9),(X . X9)] is V15() set
{( the carrier of X,T,J,X9),(X . X9)} is non empty set
{( the carrier of X,T,J,X9)} is non empty trivial 1 -element set
{{( the carrier of X,T,J,X9),(X . X9)},{( the carrier of X,T,J,X9)}} is non empty set
F is Element of the carrier of Y
h is non empty transitive directed NetStr over T
[h,p] is V15() set
{h,p} is non empty set
{h} is non empty trivial 1 -element set
{{h,p},{h}} is non empty set
the mapping of h is Relation-like the carrier of h -defined the carrier of T -valued Function-like non empty V14( the carrier of h) quasi_total Element of bool [: the carrier of h, the carrier of T:]
the carrier of h is non empty set
[: the carrier of h, the carrier of T:] is Relation-like non empty set
bool [: the carrier of h, the carrier of T:] is non empty set
rng the mapping of h is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
{ (Y . b₁) where b₁ is Element of the carrier of Y : F <= b₁ } is set
(T,X) is Element of the carrier of T
(T,X,J) is non empty transitive strict directed NetStr over T
the carrier of (T,X,J) is non empty set
the InternalRel of (T,X,J) is Relation-like the carrier of (T,X,J) -defined the carrier of (T,X,J) -valued Element of bool [: the carrier of (T,X,J), the carrier of (T,X,J):]
[: the carrier of (T,X,J), the carrier of (T,X,J):] is Relation-like non empty set
bool [: the carrier of (T,X,J), the carrier of (T,X,J):] is non empty set
RelStr(# the carrier of (T,X,J), the InternalRel of (T,X,J) #) is non empty strict RelStr
product J is non empty strict transitive directed RelStr
[:X,(product J):] is non empty strict transitive directed RelStr
the carrier of (product J) is functional non empty set
[: the carrier of X, the carrier of (product J):] is Relation-like non empty set
the Relation-like Function-like Element of the carrier of (product J) is Relation-like Function-like Element of the carrier of (product J)
the mapping of (T,X,J) is Relation-like the carrier of (T,X,J) -defined the carrier of T -valued Function-like non empty V14( the carrier of (T,X,J)) quasi_total Element of bool [: the carrier of (T,X,J), the carrier of T:]
[: the carrier of (T,X,J), the carrier of T:] is Relation-like non empty set
bool [: the carrier of (T,X,J), the carrier of T:] is non empty set
Y9 is non empty transitive directed ((T,C),M)
the mapping of Y9 is Relation-like the carrier of Y9 -defined the carrier of (T,C) -valued Function-like non empty V14( the carrier of Y9) quasi_total Element of bool [: the carrier of Y9, the carrier of (T,C):]
the carrier of Y9 is non empty set
[: the carrier of Y9, the carrier of (T,C):] is Relation-like non empty set
bool [: the carrier of Y9, the carrier of (T,C):] is non empty set
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V14( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of T:]
[: the carrier of Y, the carrier of T:] is Relation-like non empty set
bool [: the carrier of Y, the carrier of T:] is non empty set
{ b₁ where b₁ is Element of the carrier of Y : a₁ <= b₁ } is set
B is Relation-like the carrier of Y -defined Function-like non empty V14( the carrier of Y) set
proj2 B is non empty set
dom B is non empty Element of bool the carrier of Y
bool the carrier of Y is non empty set
B is set
B . B is set
M is Element of the carrier of Y
B9 is Element of the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : M <= b₁ } is set
M is Relation-like the carrier of X -defined Function-like non empty V14( the carrier of X) set
B is Relation-like non-empty non empty-yielding the carrier of Y -defined Function-like non empty V14( the carrier of Y) set
B9 is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty V14( the carrier of X) set
u is set
M . u is set
B9 . u is set
J . u is set
f is Element of the carrier of Y
f is non empty transitive directed NetStr over T
[f,p] is V15() set
{f,p} is non empty set
{f} is non empty trivial 1 -element set
{{f,p},{f}} is non empty set
the mapping of f is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty V14( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of T:]
the carrier of f is non empty set
[: the carrier of f, the carrier of T:] is Relation-like non empty set
bool [: the carrier of f, the carrier of T:] is non empty set
rng the mapping of f is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
{ (Y . b₁) where b₁ is Element of the carrier of Y : f <= b₁ } is set
m is Element of the carrier of X
B9 . m is non empty set
n is Element of the carrier of f
the mapping of f . n is set
dom the mapping of f is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
the mapping of f . n is Element of the carrier of T
p is Element of the carrier of Y
Y . p is Element of the carrier of T
the mapping of Y . p is Element of the carrier of T
{ b₁ where b₁ is Element of the carrier of Y : f <= b₁ } is set
k9 is Element of B9 . m
the mapping of Y . k9 is set
[: the carrier of f,(B9 . m):] is Relation-like non empty set
bool [: the carrier of f,(B9 . m):] is non empty set
n is Relation-like the carrier of f -defined B9 . m -valued Function-like non empty V14( the carrier of f) quasi_total Element of bool [: the carrier of f,(B9 . m):]
p is set
B . u is set
[: the carrier of f,(B . u):] is Relation-like set
bool [: the carrier of f,(B . u):] is non empty set
G is Relation-like the carrier of f -defined B . u -valued Function-like quasi_total Element of bool [: the carrier of f,(B . u):]
G . p is set
the mapping of Y . (G . p) is set
k9 is Element of the carrier of f
G . k9 is Element of B . u
( the carrier of X,T,J,m) is non empty transitive directed NetStr over T
the mapping of ( the carrier of X,T,J,m) is Relation-like the carrier of ( the carrier of X,T,J,m) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of X,T,J,m)) quasi_total Element of bool [: the carrier of ( the carrier of X,T,J,m), the carrier of T:]
the carrier of ( the carrier of X,T,J,m) is non empty set
[: the carrier of ( the carrier of X,T,J,m), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,T,J,m), the carrier of T:] is non empty set
the mapping of ( the carrier of X,T,J,m) . p is set
the mapping of f . k9 is Element of the carrier of T
u is Relation-like the carrier of X -defined Function-like non empty V14( the carrier of X) Function-yielding V136() ManySortedFunction of M,B9
f is Element of the carrier of X
u . f is Relation-like Function-like set
f is Relation-like Function-like Element of the carrier of (product J)
f . f is Element of the carrier of (J . f)
J . f is non empty RelStr
the carrier of (J . f) is non empty set
(u . f) . (f . f) is set
X9 is non empty transitive directed ((T,C)) ((T,C)) NetStr over (T,C)
the carrier of X9 is non empty set
n is Element of the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : S₃[b₁] } is set
m is Element of the carrier of X9
Carrier J is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty V14( the carrier of X) set
dom (Carrier J) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
product (Carrier J) is functional non empty with_common_domain product-like set
f . m is set
(Carrier J) . m is set
( the carrier of X,T,J,f) is non empty transitive directed NetStr over T
the carrier of ( the carrier of X,T,J,f) is non empty set
u . n is Relation-like Function-like set
M . n is set
B . n is non empty set
[:(M . n),(B . n):] is Relation-like set
bool [:(M . n),(B . n):] is non empty set
(u . n) . (f . f) is set
[:[: the carrier of X, the carrier of (product J):], the carrier of Y:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of (product J):], the carrier of Y:] is non empty set
f is Relation-like [: the carrier of X, the carrier of (product J):] -defined the carrier of Y -valued Function-like non empty V14([: the carrier of X, the carrier of (product J):]) quasi_total Element of bool [:[: the carrier of X, the carrier of (product J):], the carrier of Y:]
[: the carrier of (T,X,J), the carrier of Y:] is Relation-like non empty set
bool [: the carrier of (T,X,J), the carrier of Y:] is non empty set
m is Element of the carrier of X
M . m is set
( the carrier of X,T,J,m) is non empty transitive directed NetStr over T
the mapping of ( the carrier of X,T,J,m) is Relation-like the carrier of ( the carrier of X,T,J,m) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of X,T,J,m)) quasi_total Element of bool [: the carrier of ( the carrier of X,T,J,m), the carrier of T:]
the carrier of ( the carrier of X,T,J,m) is non empty set
[: the carrier of ( the carrier of X,T,J,m), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,T,J,m), the carrier of T:] is non empty set
u . m is Relation-like Function-like set
n is Element of M . m
the mapping of ( the carrier of X,T,J,m) . n is set
(u . m) . n is set
the mapping of Y . ((u . m) . n) is set
B9 . m is non empty set
[:(M . m),(B9 . m):] is Relation-like set
bool [:(M . m),(B9 . m):] is non empty set
p is Relation-like M . m -defined B9 . m -valued Function-like V14(M . m) quasi_total Element of bool [:(M . m),(B9 . m):]
p . n is set
the mapping of Y . (p . n) is set
k9 is Relation-like Function-like set
k9 . n is set
G is Element of the carrier of X
( the carrier of X,T,J,G) is non empty transitive directed NetStr over T
the mapping of ( the carrier of X,T,J,G) is Relation-like the carrier of ( the carrier of X,T,J,G) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of X,T,J,G)) quasi_total Element of bool [: the carrier of ( the carrier of X,T,J,G), the carrier of T:]
the carrier of ( the carrier of X,T,J,G) is non empty set
[: the carrier of ( the carrier of X,T,J,G), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,T,J,G), the carrier of T:] is non empty set
the mapping of ( the carrier of X,T,J,G) . n is set
dom the mapping of (T,X,J) is non empty Element of bool the carrier of (T,X,J)
bool the carrier of (T,X,J) is non empty set
f is Relation-like the carrier of (T,X,J) -defined the carrier of Y -valued Function-like non empty V14( the carrier of (T,X,J)) quasi_total Element of bool [: the carrier of (T,X,J), the carrier of Y:]
m is set
the mapping of (T,X,J) . m is set
f . m is set
the mapping of Y9 . (f . m) is set
X9 is non empty transitive directed ((T,C)) ((T,C)) NetStr over (T,C)
the carrier of X9 is non empty set
Carrier J is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty V14( the carrier of X) set
product (Carrier J) is functional non empty with_common_domain product-like set
[: the carrier of X9,(product (Carrier J)):] is Relation-like non empty set
[: the carrier of X9, the carrier of (product J):] is Relation-like non empty set
n is Element of the carrier of X9
p is Relation-like Function-like Element of the carrier of (product J)
[n,p] is V15() Element of the carrier of [:X9,(product J):]
[:X9,(product J):] is non empty strict transitive directed RelStr
the carrier of [:X9,(product J):] is non empty set
{n,p} is non empty set
{n} is non empty trivial 1 -element set
{{n,p},{n}} is non empty set
dom (Carrier J) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
k9 is Element of the carrier of X
( the carrier of X,T,J,k9) is non empty transitive directed NetStr over T
the carrier of ( the carrier of X,T,J,k9) is non empty set
(Carrier J) . n is set
p . n is set
M . k9 is set
the mapping of (T,X,J) . (n,p) is set
[n,p] is V15() set
the mapping of (T,X,J) . [n,p] is set
the mapping of ( the carrier of X,T,J,k9) is Relation-like the carrier of ( the carrier of X,T,J,k9) -defined the carrier of T -valued Function-like non empty V14( the carrier of ( the carrier of X,T,J,k9)) quasi_total Element of bool [: the carrier of ( the carrier of X,T,J,k9), the carrier of T:]
[: the carrier of ( the carrier of X,T,J,k9), the carrier of T:] is Relation-like non empty set
bool [: the carrier of ( the carrier of X,T,J,k9), the carrier of T:] is non empty set
the mapping of ( the carrier of X,T,J,k9) . (p . n) is set
u . k9 is Relation-like Function-like set
G is Element of M . k9
(u . k9) . G is set
the mapping of Y9 . ((u . k9) . G) is set
f . (n,p) is set
f . [n,p] is set
the mapping of Y9 . (f . (n,p)) is set
the mapping of Y * f is Relation-like the carrier of (T,X,J) -defined the carrier of T -valued Function-like non empty V14( the carrier of (T,X,J)) quasi_total Element of bool [: the carrier of (T,X,J), the carrier of T:]
dom f is non empty Element of bool the carrier of (T,X,J)
dom the mapping of Y9 is non empty Element of bool the carrier of Y9
bool the carrier of Y9 is non empty set
m is set
f . m is set
X9 is non empty transitive directed ((T,C)) ((T,C)) NetStr over (T,C)
the carrier of X9 is non empty set
Carrier J is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty V14( the carrier of X) set
product (Carrier J) is functional non empty with_common_domain product-like set
[: the carrier of X9,(product (Carrier J)):] is Relation-like non empty set
[: the carrier of X9, the carrier of (product J):] is Relation-like non empty set
m is Element of the carrier of Y
[m, the Relation-like Function-like Element of the carrier of (product J)] is V15() Element of the carrier of [:Y,(product J):]
[:Y,(product J):] is non empty strict transitive directed RelStr
the carrier of [:Y,(product J):] is non empty set
{m, the Relation-like Function-like Element of the carrier of (product J)} is non empty set
{m} is non empty trivial 1 -element set
{{m, the Relation-like Function-like Element of the carrier of (product J)},{m}} is non empty set
n is Element of the carrier of (T,X,J)
p is Element of the carrier of (T,X,J)
( the carrier of (T,X,J),Y,f,p) is Element of the carrier of Y
k9 is Element of the carrier of X
G is Relation-like Function-like Element of the carrier of (product J)
[k9,G] is V15() Element of the carrier of [:X,(product J):]
the carrier of [:X,(product J):] is non empty set
{k9,G} is non empty set
{k9} is non empty trivial 1 -element set
{{k9,G},{k9}} is non empty set
Carrier J is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty V14( the carrier of X) set
dom (Carrier J) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
X9 is non empty transitive directed ((T,C)) ((T,C)) NetStr over (T,C)
the carrier of X9 is non empty set
product (Carrier J) is functional non empty with_common_domain product-like set
f . (k9,G) is set
[k9,G] is V15() set
f . [k9,G] is set
k is Element of the carrier of Y
u . k is Relation-like Function-like set
G . k is set
(u . k) . (G . k) is set
M . k is set
B . k is non empty set
[:(M . k),(B . k):] is Relation-like set
bool [:(M . k),(B . k):] is non empty set
proj2 (u . k) is set
proj1 (u . k) is set
( the carrier of X,T,J,k9) is non empty transitive directed NetStr over T
the carrier of ( the carrier of X,T,J,k9) is non empty set
k99 is Element of the carrier of X9
(Carrier J) . k99 is set
G . k99 is set
m9 is Element of the carrier of X
F is Relation-like Function-like Element of the carrier of (product J)
[m9,F] is V15() Element of the carrier of [:X,(product J):]
{m9,F} is non empty set
{m9} is non empty trivial 1 -element set
{{m9,F},{m9}} is non empty set
k9 is Element of the carrier of X
G is Relation-like Function-like Element of the carrier of (product J)
[k9,G] is V15() Element of the carrier of [:X,(product J):]
{k9,G} is non empty set
{k9} is non empty trivial 1 -element set
{{k9,G},{k9}} is non empty set
{ b₁ where b₁ is Element of the carrier of Y : k <= b₁ } is set
c₄₃ is Element of the carrier of Y
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: 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
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr
( 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
F is non empty transitive strict directed NetStr over T
the carrier of F is non empty set
[X,q] is V15() set
{X,q} is non empty set
{X} is non empty trivial 1 -element set
{{X,q},{X}} is non empty set
[(T,X,J),q] is V15() set
{(T,X,J),q} is non empty set
{(T,X,J)} is non empty trivial 1 -element set
{{(T,X,J),q},{(T,X,J)}} is non empty set