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

bool {} is non empty 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
[:(),():] is Relation-like set
bool [:(),():] is non empty set
a is set
{a} is non empty set
a is set
aa is 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 non empty subset-closed () set
union X is set
[:(),():] is Relation-like set
bool [:(),():] is non empty set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(),():]

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
c6 is set
{c6} is non empty set
gg is set
{gg} is non empty set
{gg,c6} is non empty set
union aa is set
ii is set
ii is set
c6 is set
{c6} is non empty set
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 is set
[:(),():] is Relation-like set
bool [:(),():] 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 is set
[:(),():] is Relation-like set
bool [:(),():] 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 is set
[:(),():] is Relation-like set
bool [:(),():] 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 () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
a is set
X is non empty subset-closed () set
union X is set
bool () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(),():]
[:(),():] is Relation-like set
bool [:(),():] is non empty set
nabla () is Relation-like union X -defined union X -valued total quasi_total V27() V29() V34() Element of bool [:(),():]
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
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

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
c6 is set
gg is set
aa is set
aa \/ gg is set
[ii,c6] is V15() set
{ii,c6} is non empty set
{ii} is non empty set
{{ii,c6},{ii}} is non empty set
ii is set
ii is set
ii is set
c6 is set
gg is set
[c6,gg] is V15() set
{c6,gg} is non empty set
{c6} is non empty set
{{c6,gg},{c6}} 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
ii is non empty subset-closed () set
ii is set
c6 is set
gg is set
[c6,gg] is V15() set
{c6,gg} is non empty set
{c6} is non empty set
{{c6,gg},{c6}} is non empty set
aa is non empty subset-closed () set
ii is non empty subset-closed () set
ii is set
c6 is set
gg is set
[c6,gg] is V15() set
{c6,gg} is non empty set
{c6} is non empty set
{{c6,gg},{c6}} is non empty set
ii is set
c6 is set
gg is set
[c6,gg] is V15() set
{c6,gg} is non empty set
{c6} is non empty set
{{c6,gg},{c6}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(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
c6 is set
[ii,c6] is V15() set
{ii,c6} is non empty set
{ii} is non empty set
{{ii,c6},{ii}} is non empty set
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 [:(),():]
[:(),():] is Relation-like set
bool [:(),():] is non empty set
((),(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

(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

(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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
X is set
(X) is set
bool X is non empty set
bool (bool X) is non empty set
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
X is set
(X) is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
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

[:(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
c6 is set
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
{ b1 where b1 is Element of bool (bool a) : b1 is non empty subset-closed () set } is set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (a) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (a) : verum } is set
ii is set
ii is non empty subset-closed () Element of (a)
union ii is set
c6 is non empty subset-closed () Element of (a)
union c6 is set
Funcs ((union ii),(union c6)) is functional set
[:(union ii),(union c6):] is Relation-like set
bool [:(union ii),(union c6):] is non empty set
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

X is set
(X) is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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

[:(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
c6 is V15() set
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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 aa):] is Relation-like set
bool [:(),(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

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

{{[a,aa],ii},{[a,aa]}} is non empty set
ii is Relation-like Function-like Element of (X)
c6 is set
gg is set
{c6,gg} is non empty set
ii . c6 is set
ii . gg is set
{(ii . c6),(ii . gg)} 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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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

[[(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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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) `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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
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

[:(),():] is Relation-like set
bool [:(),():] is non empty set
[[a,a],(id ())] is V15() set
{[a,a],(id ())} is non empty set

{{[a,a],(id ())},{[a,a]}} is non empty set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

ii is set
ii is set
{ii,ii} is non empty set
(id ()) . ii is set
(id ()) . ii is set
{((id ()) . ii),((id ()) . 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],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
c6 is set
[[a,ii],c6] is V15() set
{[a,ii],c6} is non empty set

{{[a,ii],c6},{[a,ii]}} 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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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

[:(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
c6 is set
(a `2) . c6 is set
gg is set
{c6,gg} is non empty set
(a `2) . gg is set
{((a `2) . c6),((a `2) . gg)} 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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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) * (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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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)
(X,aa,a) `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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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) * (a `2) is Relation-like Function-like set
(X,(X,aa,a),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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
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 b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

[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

[:(),():] is Relation-like set
bool [:(),():] is non empty set
[[a,a],(id ())] is V15() set
{[a,a],(id ())} is non empty set

{{[a,a],(id ())},{[a,a]}} is non empty 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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

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

[:(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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

[:(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)
c6 is Element of (X)
(X,gg,c6) is Element of (X)
a is set
aa is set
ii is set
c6 is Element of (X)
ii is Element of (X)
(X,c6,ii) is Element of (X)
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)
c6 is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c6) is non empty subset-closed () Element of (X)
c6 `1 is set
(c6 `1) `2 is set
(X,c6,ii) is Element of (X)
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)
c6 is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c6) is non empty subset-closed () Element of (X)
c6 `1 is set
(c6 `1) `2 is set
(X,c6,ii) is Element of (X)
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
c6 is Element of (X)
(X,c6) is non empty subset-closed () Element of (X)
c6 `1 is set
(c6 `1) `1 is set
gg is Element of (X)
(X,gg) is non empty subset-closed () Element of (X)
gg `1 is set
(gg `1) `2 is set
c6 is Element of (X)
(X,c6) is non empty subset-closed () Element of (X)
c6 `1 is set
(c6 `1) `1 is set
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)
c6 is Element of (X)
[ii,c6] is V15() set
{ii,c6} is non empty set
{ii} is non empty set
{{ii,c6},{ii}} is non empty set
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c6) is non empty subset-closed () Element of (X)
c6 `1 is set
(c6 `1) `2 is set
a . [ii,c6] is set
(X,c6,ii) is Element of (X)
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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

(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
{ b1 where b1 is Element of bool (bool X) : b1 is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b1),(union b2))) where b1, b2 is non empty subset-closed () Element of (X) : verum } is set
{ [[b1,b2],b3] where b1, b2 is non empty subset-closed () Element of (X), b3 is Relation-like Function-like Element of (X) : ( ( not union b2 = {} or union b1 = {} ) & b3 is Relation-like union b1 -defined union b2 -valued Function-like quasi_total Element of bool [:(union b1),(union b2):] & ( for b4, b5 being set holds
( not {b4,b5} in b1 or {(b3 . b4),(b3 . b5)} in b2 ) ) )
}
is set

(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