:: COH_SP semantic presentation

K132() is Element of bool K128()

K128() is set

bool K128() is non empty set

K114() is set

bool K114() is non empty set

bool K132() is non empty set

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

bool {} is non empty set

{{}} is functional non empty set

union {} is set

[:{},{}:] is Relation-like set

bool [:{},{}:] is non empty set

X is functional non empty set

a is set

aa is set

a is set

union a is set

X is non empty subset-closed () set

a is set

aa is set

a \/ aa is set

X is set

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

a is set

union a is set

aa is set

a is set

aa is set

X is set

{X} is non empty set

a is non empty subset-closed () set

union a is set

aa is set

X is non empty subset-closed () set

union X is set

[:(union X),(union X):] is Relation-like set

bool [:(union X),(union X):] is non empty set

a is set

{a} is non empty set

a is set

aa is set

ii is set

a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

ii is set

a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

aa is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

X is non empty subset-closed () set

union X is set

[:(union X),(union X):] is Relation-like set

bool [:(union X),(union X):] is non empty set

(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

ii is set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

ii is set

X is set

a is non empty subset-closed () set

aa is set

ii is set

{aa,ii} is non empty set

aa is set

{aa} is non empty set

ii is set

ii is set

aa is set

ii is set

ii is set

ii \/ ii is set

c

{c

gg is set

{gg} is non empty set

{gg,c

union aa is set

ii is set

ii is set

c

{c

ii is set

{ii} is non empty set

ii is set

ii is set

{ii} is non empty set

{ii,ii} is non empty set

X is set

a is non empty subset-closed () set

(a) is Relation-like union a -defined union a -valued total quasi_total V27() V29() Element of bool [:(union a),(union a):]

union a is set

[:(union a),(union a):] is Relation-like set

bool [:(union a),(union a):] is non empty set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

X is set

a is non empty subset-closed () set

union a is set

aa is set

{aa,aa} is non empty set

{aa} is non empty set

X is non empty subset-closed () set

(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

union X is set

[:(union X),(union X):] is Relation-like set

bool [:(union X),(union X):] is non empty set

a is non empty subset-closed () set

(a) is Relation-like union a -defined union a -valued total quasi_total V27() V29() Element of bool [:(union a),(union a):]

union a is set

[:(union a),(union a):] is Relation-like set

bool [:(union a),(union a):] is non empty set

aa is set

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is set

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

X is non empty subset-closed () set

union X is set

bool (union X) is non empty Element of bool (bool (union X))

bool (union X) is non empty set

bool (bool (union X)) is non empty set

a is set

X is non empty subset-closed () set

union X is set

bool (union X) is non empty Element of bool (bool (union X))

bool (union X) is non empty set

bool (bool (union X)) is non empty set

(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

[:(union X),(union X):] is Relation-like set

bool [:(union X),(union X):] is non empty set

nabla (union X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() V34() Element of bool [:(union X),(union X):]

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

ii is set

X is set

[:X,X:] is Relation-like set

bool [:X,X:] is non empty set

a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

aa is set

ii is set

union ii is set

ii is set

c

gg is set

aa is set

aa \/ gg is set

[ii,c

{ii,c

{ii} is non empty set

{{ii,c

ii is set

ii is set

ii is set

c

gg is set

[c

{c

{c

{{c

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

ii is non empty subset-closed () set

ii is set

c

gg is set

[c

{c

{c

{{c

aa is non empty subset-closed () set

ii is non empty subset-closed () set

ii is set

c

gg is set

[c

{c

{c

{{c

ii is set

c

gg is set

[c

{c

{c

{{c

X is set

[:X,X:] is Relation-like set

bool [:X,X:] is non empty set

a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]

(X,a) is non empty subset-closed () set

((X,a)) is Relation-like union (X,a) -defined union (X,a) -valued total quasi_total V27() V29() Element of bool [:(union (X,a)),(union (X,a)):]

union (X,a) is set

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

ii is set

c

[ii,c

{ii,c

{ii} is non empty set

{{ii,c

X is non empty subset-closed () set

union X is set

(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]

[:(union X),(union X):] is Relation-like set

bool [:(union X),(union X):] is non empty set

((union X),(X)) is non empty subset-closed () set

a is set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

a is set

aa is set

ii is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

X is set

[:X,X:] is Relation-like set

bool [:X,X:] is non empty set

a is set

aa is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]

(X,aa) is non empty subset-closed () set

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

X is set

[:X,X:] is Relation-like set

bool [:X,X:] is non empty set

a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]

(X,a) is non empty subset-closed () set

TolSets a is set

aa is set

aa is set

X is set

bool X is non empty set

bool (bool X) is non empty set

{ b

X is set

(X) is set

bool X is non empty set

bool (bool X) is non empty set

{ b

bool X is non empty Element of bool (bool X)

a is Element of bool (bool X)

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

a is Element of (X)

aa is Element of bool (bool X)

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

a is set

aa is set

{a,aa} is non empty set

ii is non empty subset-closed () Element of (X)

union ii is set

{a} is non empty set

{aa} is non empty set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

{ (Funcs ((union b

union { (Funcs ((union b

X is set

(X) is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

{ (Funcs ((union b

union { (Funcs ((union b

bool X is non empty Element of bool (bool X)

a is Element of bool (bool X)

aa is non empty subset-closed () Element of (X)

union aa is set

id (union aa) is Relation-like union aa -defined union aa -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union aa),(union aa):]

[:(union aa),(union aa):] is Relation-like set

bool [:(union aa),(union aa):] is non empty set

Funcs ((union aa),(union aa)) is functional non empty set

c

ii is non empty set

gg is set

aa is non empty subset-closed () Element of (X)

union aa is set

ii is non empty subset-closed () Element of (X)

union ii is set

Funcs ((union aa),(union ii)) is functional set

X is set

a is set

(a) is functional non empty set

(a) is non empty set

bool a is non empty set

bool (bool a) is non empty set

{ b

{ (Funcs ((union b

union { (Funcs ((union b

ii is set

ii is non empty subset-closed () Element of (a)

union ii is set

c

union c

Funcs ((union ii),(union c

[:(union ii),(union c

bool [:(union ii),(union c

ii is non empty subset-closed () Element of (a)

union ii is set

ii is non empty subset-closed () Element of (a)

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

Funcs ((union ii),(union ii)) is functional set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

X is set

(X) is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

bool X is non empty Element of bool (bool X)

aa is Element of bool (bool X)

ii is non empty subset-closed () Element of (X)

union ii is set

id (union ii) is Relation-like union ii -defined union ii -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union ii),(union ii):]

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

[[ii,ii],(id (union ii))] is V15() set

{[ii,ii],(id (union ii))} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],(id (union ii))},{[ii,ii]}} is non empty set

aa is set

ii is set

{aa,ii} is non empty set

gg is Relation-like Function-like Element of (X)

gg . aa is set

gg . ii is set

{(gg . aa),(gg . ii)} is non empty set

c

aa is V15() set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

aa is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

ii is Relation-like Function-like Element of (X)

[[aa,ii],ii] is V15() set

{[aa,ii],ii} is non empty set

{[aa,ii]} is Relation-like Function-like non empty set

{{[aa,ii],ii},{[aa,ii]}} is non empty set

union ii is set

union aa is set

[:(union aa),(union ii):] is Relation-like set

bool [:(union aa),(union ii):] is non empty set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is non empty set

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is non empty subset-closed () Element of (X)

union a is set

aa is non empty subset-closed () Element of (X)

union aa is set

[:(union a),(union aa):] is Relation-like set

bool [:(union a),(union aa):] is non empty set

[a,aa] is V15() set

{a,aa} is non empty set

{a} is non empty set

{{a,aa},{a}} is non empty set

ii is Relation-like union a -defined union aa -valued Function-like quasi_total Element of bool [:(union a),(union aa):]

[[a,aa],ii] is V15() set

{[a,aa],ii} is non empty set

{[a,aa]} is Relation-like Function-like non empty set

{{[a,aa],ii},{[a,aa]}} is non empty set

ii is Relation-like Function-like Element of (X)

c

gg is set

{c

ii . c

ii . gg is set

{(ii . c

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

a `2 is set

ii is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is Relation-like Function-like Element of (X)

[[ii,ii],aa] is V15() set

{[ii,ii],aa} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],aa},{[ii,ii]}} is non empty set

union ii is set

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[[ii,ii],aa] `2 is set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

a `1 is set

(a `1) `1 is set

ii is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is Relation-like Function-like Element of (X)

[[ii,ii],aa] is V15() set

{[ii,ii],aa} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],aa},{[ii,ii]}} is non empty set

union ii is set

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[[ii,ii],aa] `1 is set

[ii,ii] `1 is set

(a `1) `2 is set

ii is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is Relation-like Function-like Element of (X)

[[ii,ii],aa] is V15() set

{[ii,ii],aa} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],aa},{[ii,ii]}} is non empty set

union ii is set

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[[ii,ii],aa] `1 is set

[ii,ii] `2 is set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `1 is set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `2 is set

[(X,a),(X,a)] is V15() set

{(X,a),(X,a)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,a)},{(X,a)}} is non empty set

a `2 is Relation-like Function-like set

[[(X,a),(X,a)],(a `2)] is V15() set

{[(X,a),(X,a)],(a `2)} is non empty set

{[(X,a),(X,a)]} is Relation-like Function-like non empty set

{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set

ii is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is Relation-like Function-like Element of (X)

[[ii,ii],aa] is V15() set

{[ii,ii],aa} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],aa},{[ii,ii]}} is non empty set

union ii is set

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[[ii,ii],aa] `1 is set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

a `2 is Relation-like Function-like set

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `1 is set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `2 is set

aa is Element of (X)

aa `2 is Relation-like Function-like set

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `1 is set

(X,aa) is non empty subset-closed () Element of (X)

(aa `1) `2 is set

[(X,a),(X,a)] is V15() set

{(X,a),(X,a)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,a)},{(X,a)}} is non empty set

[[(X,a),(X,a)],(a `2)] is V15() set

{[(X,a),(X,a)],(a `2)} is non empty set

{[(X,a),(X,a)]} is Relation-like Function-like non empty set

{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

a is non empty subset-closed () Element of (X)

[a,a] is V15() set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

union a is set

id (union a) is Relation-like union a -defined union a -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union a),(union a):]

[:(union a),(union a):] is Relation-like set

bool [:(union a),(union a):] is non empty set

[[a,a],(id (union a))] is V15() set

{[a,a],(id (union a))} is non empty set

{[a,a]} is Relation-like Function-like non empty set

{{[a,a],(id (union a))},{[a,a]}} is non empty set

(X) is non empty set

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

ii is set

ii is set

{ii,ii} is non empty set

(id (union a)) . ii is set

(id (union a)) . ii is set

{((id (union a)) . ii),((id (union a)) . ii)} is non empty set

X is set

aa is set

[X,aa] is V15() set

{X,aa} is non empty set

{X} is non empty set

{{X,aa},{X}} is non empty set

ii is set

[[X,aa],ii] is V15() set

{[X,aa],ii} is non empty set

{[X,aa]} is Relation-like Function-like non empty set

{{[X,aa],ii},{[X,aa]}} is non empty set

a is set

ii is set

[a,ii] is V15() set

{a,ii} is non empty set

{a} is non empty set

{{a,ii},{a}} is non empty set

c

[[a,ii],c

{[a,ii],c

{[a,ii]} is Relation-like Function-like non empty set

{{[a,ii],c

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `2 is set

union (X,a) is set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `1 is set

union (X,a) is set

a `2 is Relation-like Function-like set

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

ii is non empty subset-closed () Element of (X)

ii is non empty subset-closed () Element of (X)

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

aa is Relation-like Function-like Element of (X)

[[ii,ii],aa] is V15() set

{[ii,ii],aa} is non empty set

{[ii,ii]} is Relation-like Function-like non empty set

{{[ii,ii],aa},{[ii,ii]}} is non empty set

union ii is set

union ii is set

[:(union ii),(union ii):] is Relation-like set

bool [:(union ii),(union ii):] is non empty set

[(X,a),(X,a)] is V15() set

{(X,a),(X,a)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,a)},{(X,a)}} is non empty set

[[(X,a),(X,a)],(a `2)] is V15() set

{[(X,a),(X,a)],(a `2)} is non empty set

{[(X,a),(X,a)]} is Relation-like Function-like non empty set

{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set

c

(a `2) . c

gg is set

{c

(a `2) . gg is set

{((a `2) . c

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `2 is set

aa is Element of (X)

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `1 is set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `1 is set

(X,aa) is non empty subset-closed () Element of (X)

(aa `1) `2 is set

[(X,a),(X,aa)] is V15() set

{(X,a),(X,aa)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,aa)},{(X,a)}} is non empty set

a `2 is Relation-like Function-like set

aa `2 is Relation-like Function-like set

(a `2) * (aa `2) is Relation-like Function-like set

[[(X,a),(X,aa)],((a `2) * (aa `2))] is V15() set

{[(X,a),(X,aa)],((a `2) * (aa `2))} is non empty set

{[(X,a),(X,aa)]} is Relation-like Function-like non empty set

{{[(X,a),(X,aa)],((a `2) * (aa `2))},{[(X,a),(X,aa)]}} is non empty set

union (X,aa) is set

union (X,aa) is set

union (X,a) is set

union (X,a) is set

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

ii is set

ii is set

{ii,ii} is non empty set

proj1 (a `2) is set

(a `2) . ii is set

(a `2) . ii is set

{((a `2) . ii),((a `2) . ii)} is non empty set

(aa `2) . ((a `2) . ii) is set

(aa `2) . ((a `2) . ii) is set

{((aa `2) . ((a `2) . ii)),((aa `2) . ((a `2) . ii))} is non empty set

((a `2) * (aa `2)) . ii is set

{(((a `2) * (aa `2)) . ii),((aa `2) . ((a `2) . ii))} is non empty set

((a `2) * (aa `2)) . ii is set

{(((a `2) * (aa `2)) . ii),(((a `2) * (aa `2)) . ii)} is non empty set

[:(union (X,aa)),(union (X,aa)):] is Relation-like set

bool [:(union (X,aa)),(union (X,aa)):] is non empty set

[:(union (X,a)),(union (X,aa)):] is Relation-like set

bool [:(union (X,a)),(union (X,aa)):] is non empty set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `1 is set

a `2 is Relation-like Function-like set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `2 is set

aa is Element of (X)

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `2 is set

(X,aa,a) is Element of (X)

(X,aa,a) `2 is Relation-like Function-like set

aa `2 is Relation-like Function-like set

(aa `2) * (a `2) is Relation-like Function-like set

(X,(X,aa,a)) is non empty subset-closed () Element of (X)

(X,aa,a) `1 is set

((X,aa,a) `1) `1 is set

(X,aa) is non empty subset-closed () Element of (X)

(aa `1) `1 is set

(X,(X,aa,a)) is non empty subset-closed () Element of (X)

((X,aa,a) `1) `2 is set

[(X,aa),(X,a)] is V15() set

{(X,aa),(X,a)} is non empty set

{(X,aa)} is non empty set

{{(X,aa),(X,a)},{(X,aa)}} is non empty set

[[(X,aa),(X,a)],((aa `2) * (a `2))] is V15() set

{[(X,aa),(X,a)],((aa `2) * (a `2))} is non empty set

{[(X,aa),(X,a)]} is Relation-like Function-like non empty set

{{[(X,aa),(X,a)],((aa `2) * (a `2))},{[(X,aa),(X,a)]}} is non empty set

[(X,(X,aa,a)),(X,(X,aa,a))] is V15() set

{(X,(X,aa,a)),(X,(X,aa,a))} is non empty set

{(X,(X,aa,a))} is non empty set

{{(X,(X,aa,a)),(X,(X,aa,a))},{(X,(X,aa,a))}} is non empty set

[[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)] is V15() set

{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)} is non empty set

{[(X,(X,aa,a)),(X,(X,aa,a))]} is Relation-like Function-like non empty set

{{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)},{[(X,(X,aa,a)),(X,(X,aa,a))]}} is non empty set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `1 is set

(X,a) is non empty subset-closed () Element of (X)

(a `1) `2 is set

aa is Element of (X)

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `2 is set

(X,aa,a) is Element of (X)

ii is Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `1 is set

(X,(X,aa,a),ii) is Element of (X)

(X,a,ii) is Element of (X)

(X,aa,(X,a,ii)) is Element of (X)

(X,(X,aa,a)) is non empty subset-closed () Element of (X)

(X,aa,a) `1 is set

((X,aa,a) `1) `2 is set

(X,aa,a) `2 is Relation-like Function-like set

aa `2 is Relation-like Function-like set

a `2 is Relation-like Function-like set

(aa `2) * (a `2) is Relation-like Function-like set

(X,(X,aa,a),ii) `2 is Relation-like Function-like set

ii `2 is Relation-like Function-like set

((aa `2) * (a `2)) * (ii `2) is Relation-like Function-like set

(X,(X,a,ii)) is non empty subset-closed () Element of (X)

(X,a,ii) `1 is set

((X,a,ii) `1) `1 is set

(X,(X,aa,(X,a,ii))) is non empty subset-closed () Element of (X)

(X,aa,(X,a,ii)) `1 is set

((X,aa,(X,a,ii)) `1) `1 is set

(X,aa) is non empty subset-closed () Element of (X)

(aa `1) `1 is set

(X,(X,aa,a)) is non empty subset-closed () Element of (X)

((X,aa,a) `1) `1 is set

(X,(X,(X,aa,a),ii)) is non empty subset-closed () Element of (X)

(X,(X,aa,a),ii) `1 is set

((X,(X,aa,a),ii) `1) `1 is set

(X,(X,a,ii)) is non empty subset-closed () Element of (X)

((X,a,ii) `1) `2 is set

(X,ii) is non empty subset-closed () Element of (X)

(ii `1) `2 is set

(X,(X,aa,(X,a,ii))) is non empty subset-closed () Element of (X)

((X,aa,(X,a,ii)) `1) `2 is set

(X,a,ii) `2 is Relation-like Function-like set

(a `2) * (ii `2) is Relation-like Function-like set

(X,aa,(X,a,ii)) `2 is Relation-like Function-like set

(aa `2) * ((a `2) * (ii `2)) is Relation-like Function-like set

(X,(X,(X,aa,a),ii)) is non empty subset-closed () Element of (X)

((X,(X,aa,a),ii) `1) `2 is set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

a is non empty subset-closed () Element of (X)

(X,a) is Element of (X)

(X) is non empty set

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

[a,a] is V15() set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

union a is set

id (union a) is Relation-like union a -defined union a -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union a),(union a):]

[:(union a),(union a):] is Relation-like set

bool [:(union a),(union a):] is non empty set

[[a,a],(id (union a))] is V15() set

{[a,a],(id (union a))} is non empty set

{[a,a]} is Relation-like Function-like non empty set

{{[a,a],(id (union a))},{[a,a]}} is non empty set

(X,a) `2 is Relation-like Function-like set

(X,(X,a)) is non empty subset-closed () Element of (X)

(X,a) `1 is set

((X,a) `1) `1 is set

(X,(X,a)) is non empty subset-closed () Element of (X)

((X,a) `1) `2 is set

[(X,(X,a)),(X,(X,a))] is V15() set

{(X,(X,a)),(X,(X,a))} is non empty set

{(X,(X,a))} is non empty set

{{(X,(X,a)),(X,(X,a))},{(X,(X,a))}} is non empty set

[[(X,(X,a)),(X,(X,a))],((X,a) `2)] is V15() set

{[(X,(X,a)),(X,(X,a))],((X,a) `2)} is non empty set

{[(X,(X,a)),(X,(X,a))]} is Relation-like Function-like non empty set

{{[(X,(X,a)),(X,(X,a))],((X,a) `2)},{[(X,(X,a)),(X,(X,a))]}} is non empty set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

a is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

a `1 is set

(a `1) `1 is set

(X,(X,a)) is Element of (X)

[(X,a),(X,a)] is V15() set

{(X,a),(X,a)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,a)},{(X,a)}} is non empty set

union (X,a) is set

id (union (X,a)) is Relation-like union (X,a) -defined union (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union (X,a)),(union (X,a)):]

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

[[(X,a),(X,a)],(id (union (X,a)))] is V15() set

{[(X,a),(X,a)],(id (union (X,a)))} is non empty set

{[(X,a),(X,a)]} is Relation-like Function-like non empty set

{{[(X,a),(X,a)],(id (union (X,a)))},{[(X,a),(X,a)]}} is non empty set

(X,(X,(X,a)),a) is Element of (X)

(X,a) is non empty subset-closed () Element of (X)

(a `1) `2 is set

(X,(X,a)) is Element of (X)

[(X,a),(X,a)] is V15() set

{(X,a),(X,a)} is non empty set

{(X,a)} is non empty set

{{(X,a),(X,a)},{(X,a)}} is non empty set

union (X,a) is set

id (union (X,a)) is Relation-like union (X,a) -defined union (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union (X,a)),(union (X,a)):]

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

[[(X,a),(X,a)],(id (union (X,a)))] is V15() set

{[(X,a),(X,a)],(id (union (X,a)))} is non empty set

{[(X,a),(X,a)]} is Relation-like Function-like non empty set

{{[(X,a),(X,a)],(id (union (X,a)))},{[(X,a),(X,a)]}} is non empty set

(X,a,(X,(X,a))) is Element of (X)

(X,(X,a)) `2 is Relation-like Function-like set

(X,(X,(X,a))) is non empty subset-closed () Element of (X)

(X,(X,a)) `1 is set

((X,(X,a)) `1) `1 is set

a `2 is Relation-like Function-like set

[:(union (X,a)),(union (X,a)):] is Relation-like set

bool [:(union (X,a)),(union (X,a)):] is non empty set

proj2 (a `2) is set

proj1 (a `2) is set

(X,(X,(X,a))) is non empty subset-closed () Element of (X)

((X,(X,a)) `1) `2 is set

(X,(X,(X,(X,a)),a)) is non empty subset-closed () Element of (X)

(X,(X,(X,a)),a) `1 is set

((X,(X,(X,a)),a) `1) `2 is set

(X,(X,(X,a)),a) `2 is Relation-like Function-like set

((X,(X,a)) `2) * (a `2) is Relation-like Function-like set

(X,(X,(X,(X,a)),a)) is non empty subset-closed () Element of (X)

((X,(X,(X,a)),a) `1) `1 is set

(X,(X,a)) `2 is Relation-like Function-like set

(X,(X,(X,a))) is non empty subset-closed () Element of (X)

(X,(X,a)) `1 is set

((X,(X,a)) `1) `2 is set

(X,(X,(X,a))) is non empty subset-closed () Element of (X)

((X,(X,a)) `1) `1 is set

(X,(X,a,(X,(X,a)))) is non empty subset-closed () Element of (X)

(X,a,(X,(X,a))) `1 is set

((X,a,(X,(X,a))) `1) `2 is set

(X,a,(X,(X,a))) `2 is Relation-like Function-like set

(a `2) * ((X,(X,a)) `2) is Relation-like Function-like set

(X,(X,a,(X,(X,a)))) is non empty subset-closed () Element of (X)

((X,a,(X,(X,a))) `1) `1 is set

X is set

(X) is non empty set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

[:(X),(X):] is Relation-like non empty set

bool [:(X),(X):] is non empty set

a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

ii is Element of (X)

a . ii is non empty subset-closed () Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `1 is set

aa . ii is non empty subset-closed () Element of (X)

a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

ii is Element of (X)

a . ii is non empty subset-closed () Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `2 is set

aa . ii is non empty subset-closed () Element of (X)

[:(X),(X):] is Relation-like non empty set

[:[:(X),(X):],(X):] is Relation-like non empty set

bool [:[:(X),(X):],(X):] is non empty set

a is set

aa is set

ii is set

ii is set

gg is Element of (X)

c

(X,gg,c

a is set

aa is set

ii is set

c

ii is Element of (X)

(X,c

a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]

dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]

bool [:(X),(X):] is non empty set

aa is Element of (X)

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `1 is set

ii is Element of (X)

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `2 is set

ii is set

(X,ii,aa) is Element of (X)

ii is Element of (X)

c

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `1 is set

(X,c

c

(c

(X,c

aa is Element of (X)

(X,aa) is non empty subset-closed () Element of (X)

aa `1 is set

(aa `1) `1 is set

ii is Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `2 is set

[aa,ii] is V15() set

{aa,ii} is non empty set

{aa} is non empty set

{{aa,ii},{aa}} is non empty set

a . [aa,ii] is set

(X,ii,aa) is Element of (X)

a . (aa,ii) is set

ii is Element of (X)

c

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `1 is set

(X,c

c

(c

(X,c

a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]

dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]

bool [:(X),(X):] is non empty set

aa is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]

dom aa is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]

ii is set

ii is set

[ii,ii] is V15() set

{ii,ii} is non empty set

{ii} is non empty set

{{ii,ii},{ii}} is non empty set

c

(X,c

c

(c

gg is Element of (X)

(X,gg) is non empty subset-closed () Element of (X)

gg `1 is set

(gg `1) `2 is set

c

(X,c

c

(c

gg is Element of (X)

(X,gg) is non empty subset-closed () Element of (X)

gg `1 is set

(gg `1) `2 is set

ii is Element of [:(X),(X):]

ii is Element of (X)

c

[ii,c

{ii,c

{ii} is non empty set

{{ii,c

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `1 is set

(X,c

c

(c

a . [ii,c

(X,c

a . ii is set

aa . ii is set

X is set

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is non empty set

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

[:(X),(X):] is Relation-like non empty set

bool [:(X),(X):] is non empty set

(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]

[:(X),(X):] is Relation-like non empty set

[:[:(X),(X):],(X):] is Relation-like non empty set

bool [:[:(X),(X):],(X):] is non empty set

CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr

X is set

(X) is non empty non void strict CatStr

(X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

{ b

(X) is non empty set

(X) is functional non empty set

{ (Funcs ((union b

union { (Funcs ((union b

{ [[b

( not {b

(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

[:(X),(X):] is Relation-like non empty set

bool [:(X),(X):] is non empty set

(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]

(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]

[:(X),(X):] is Relation-like non empty set

[:[:(X),(X):],(X):] is Relation-like non empty set

bool [:[:(X),(X):],(X):] is non empty set

CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr

the carrier' of (X) is set

aa is Element of the carrier' of (X)

gg is Element of the carrier' of (X)

[aa,gg] is V15() set

{aa,gg} is non empty set

{aa} is non empty set

{{aa,gg},{aa}} is non empty set

the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]

[: the carrier' of (X), the carrier' of (X):] is Relation-like set

[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set

bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set

proj1 the Comp of (X) is Relation-like set

dom aa is Element of the carrier of (X)

the carrier of (X) is set

the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

[: the carrier' of (X), the carrier of (X):] is Relation-like set

bool [: the carrier' of (X), the carrier of (X):] is non empty set

the Source of (X) . aa is Element of the carrier of (X)

cod gg is Element of the carrier of (X)

the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

the Target of (X) . gg is Element of the carrier of (X)

(X) . aa is set

f is Element of (X)

(X,f) is non empty subset-closed () Element of (X)

f `1 is set

(f `1) `1 is set

(X) . gg is set

ii is Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `2 is set

the carrier' of (X) is set

aa is Element of the carrier' of (X)

dom aa is Element of the carrier of (X)

the carrier of (X) is set

the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

[: the carrier' of (X), the carrier of (X):] is Relation-like set

bool [: the carrier' of (X), the carrier of (X):] is non empty set

the Source of (X) . aa is Element of the carrier of (X)

gg is Element of the carrier' of (X)

cod gg is Element of the carrier of (X)

the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

the Target of (X) . gg is Element of the carrier of (X)

aa (*) gg is Element of the carrier' of (X)

dom (aa (*) gg) is Element of the carrier of (X)

the Source of (X) . (aa (*) gg) is Element of the carrier of (X)

dom gg is Element of the carrier of (X)

the Source of (X) . gg is Element of the carrier of (X)

cod (aa (*) gg) is Element of the carrier of (X)

the Target of (X) . (aa (*) gg) is Element of the carrier of (X)

cod aa is Element of the carrier of (X)

the Target of (X) . aa is Element of the carrier of (X)

[aa,gg] is V15() set

{aa,gg} is non empty set

{aa} is non empty set

{{aa,gg},{aa}} is non empty set

[: the carrier' of (X), the carrier' of (X):] is Relation-like set

the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]

[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set

bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set

dom the Comp 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):]

bool [: the carrier' of (X), the carrier' of (X):] is non empty set

the Comp of (X) . (aa,gg) is set

the Comp of (X) . [aa,gg] is set

f is Element of (X)

(X) . f is non empty subset-closed () Element of (X)

(X,f) is non empty subset-closed () Element of (X)

f `1 is set

(f `1) `1 is set

ii is Element of (X)

(X) . ii is non empty subset-closed () Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

ii `1 is set

(ii `1) `2 is set

[f,ii] is V15() set

{f,ii} is non empty set

{f} is non empty set

{{f,ii},{f}} is non empty set

(X) . [f,ii] is set

(X,ii,f) is Element of (X)

(X) . ii is non empty subset-closed () Element of (X)

(X,ii) is non empty subset-closed () Element of (X)

(ii `1) `1 is set

(X) . f is non empty subset-closed () Element of (X)

(X,f) is non empty subset-closed () Element of (X)

(f `1) `2 is set

(X,(X,ii,f)) is non empty subset-closed () Element of (X)

(X,ii,f) `1 is set

((X,ii,f) `1) `1 is set

(X,(X,ii,f)) is non empty subset-closed () Element of (X)

((X,ii,f) `1) `2 is set

the carrier' of (X) is set

ii is Element of the carrier' of (X)

dom ii is Element of the carrier of (X)

the carrier of (X) is set

the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]

[: the carrier' of (X), the carrier of (X):] is Relation-like set

bool [: the carrier' of (X), the carrier of (X):] is non empty set

the Source of (X) . ii is Element of the carrier of (X)

aa is Element of the carrier' of (X)

cod aa is Element of the carrier of (X)

the