:: 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₆ is set
{c₆} is non empty set
gg is set
{gg} is non empty set
{gg,c₆} is non empty set
union aa is set
ii is set
ii is set
c₆ is set
{c₆} 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),(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₆ is set
gg is set
aa is set
aa \/ gg is set
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{ii}} is non empty set
ii is set
ii is set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} 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
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
aa is non empty subset-closed () set
ii is non empty subset-closed () set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} 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
((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₆ is set
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{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 [:(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₁ where b₁ is Element of bool (bool X) : b₁ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ 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
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₆ 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
{ b₁ where b₁ is Element of bool (bool a) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (a) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ 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
c₆ is non empty subset-closed () Element of (a)
union c₆ is set
Funcs ((union ii),(union c₆)) is functional set
[:(union ii),(union c₆):] is Relation-like set
bool [:(union ii),(union c₆):] 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
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₆ 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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 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₆ is set
gg is set
{c₆,gg} is non empty set
ii . c₆ is set
ii . gg is set
{(ii . c₆),(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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } 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
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<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
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₁ where b₁ is Element of bool (bool X) : b₁ 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
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 b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
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₆ is set
[[a,ii],c₆] is V15() set
{[a,ii],c₆} is non empty set
{[a,ii]} is Relation-like Function-like non empty set
{{[a,ii],c₆},{[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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
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<sub>6</sub> is set
(a `2) . c₆ is set
gg is set
{c₆,gg} is non empty set
(a `2) . gg is set
{((a `2) . c₆),((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
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } 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 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₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
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<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } 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 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<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> 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 b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } 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
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₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
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₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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)
c₆ is Element of (X)
(X,gg,c₆) is Element of (X)
a is set
aa is set
ii is set
c₆ is Element of (X)
ii is Element of (X)
(X,c₆,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)
c₆ is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,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)
c₆ is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,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
c₆ is Element of (X)
(X,c₆) is non empty subset-closed () Element of (X)
c₆ `1 is set
(c<sub>6</sub> `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
c₆ is Element of (X)
(X,c₆) is non empty subset-closed () Element of (X)
c₆ `1 is set
(c<sub>6</sub> `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)
c₆ is Element of (X)
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{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,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
a . [ii,c₆] is set
(X,c₆,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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } 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