:: COHSP_1 semantic presentation

REAL is set
NAT is non empty non trivial V8() V9() V10() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
NAT is non empty non trivial V8() V9() V10() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set
K262() is L6()
the U1 of K262() is set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set
{} is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
the empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
1 is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
2 is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
3 is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
bool {} is non empty cup-closed diff-closed preBoolean finite V41() set
{{}} is non empty trivial finite V41() 1 -element set
union {} is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal set
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V41() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty finite V41() set
C1 is non empty set
C2 is non empty set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed diff-closed preBoolean set
x2 is set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
y1 is Element of C1
x1 . y1 is Element of C2
union C2 is set
C1 is set
C2 is set
union C2 is set
x1 is set
x1 \/ x1 is set
C2 is set
union C2 is set
C1 is set
id C1 is Relation-like C1 -defined C1 -valued V30(C1) V57() V59() V60() V64() Element of bool [:C1,C1:]
[:C1,C1:] is Relation-like set
bool [:C1,C1:] is non empty cup-closed diff-closed preBoolean set
CohSp (id C1) is non empty subset-closed binary_complete set
bool C1 is non empty cup-closed diff-closed preBoolean set
C2 is Element of bool C1
x1 is Element of bool C1
y1 is set
C2 is set
C1 is set
(C1) is set
id C1 is Relation-like C1 -defined C1 -valued V30(C1) V57() V59() V60() V64() Element of bool [:C1,C1:]
[:C1,C1:] is Relation-like set
bool [:C1,C1:] is non empty cup-closed diff-closed preBoolean set
CohSp (id C1) is non empty subset-closed binary_complete set
x1 is non empty set
the Element of x1 is Element of x1
x2 is set
y2 is set
{y2} is non empty trivial finite 1 -element set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{{y2,x},{y2}} is non empty finite V41() set
[y2,y2] is V31() set
{y2,y2} is non empty finite set
{{y2,y2},{y2}} is non empty finite V41() set
x1 is set
{x1} is non empty trivial finite 1 -element set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
x1 is set
{x1} is non empty trivial finite 1 -element set
C1 is set
(C1) is set
id C1 is Relation-like C1 -defined C1 -valued V30(C1) V57() V59() V60() V64() Element of bool [:C1,C1:]
[:C1,C1:] is Relation-like set
bool [:C1,C1:] is non empty cup-closed diff-closed preBoolean set
CohSp (id C1) is non empty subset-closed binary_complete set
union (C1) is set
C2 is set
x1 is set
y1 is set
{y1} is non empty trivial finite 1 -element set
C2 is set
{C2} is non empty trivial finite 1 -element set
C1 is finite subset-closed set
(C1) is finite Element of bool C1
bool C1 is non empty cup-closed diff-closed preBoolean finite V41() set
C2 is set
bool C2 is non empty cup-closed diff-closed preBoolean set
x1 is set
C1 is set
bool C1 is non empty cup-closed diff-closed preBoolean set
(C1) is set
id C1 is Relation-like C1 -defined C1 -valued V30(C1) V57() V59() V60() V64() Element of bool [:C1,C1:]
[:C1,C1:] is Relation-like set
bool [:C1,C1:] is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
CohSp (id C1) is non empty subset-closed binary_complete set
C1 is non empty subset-closed set
(C1) is Element of bool C1
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
the Element of C1 is Element of C1
x1 is set
y1 is set
Web {{}} is Relation-like union {{}} -defined union {{}} -valued V30( union {{}}) finite V57() V59() Element of bool [:(union {{}}),(union {{}}):]
union {{}} is finite set
[:(union {{}}),(union {{}}):] is Relation-like finite set
bool [:(union {{}}),(union {{}}):] is non empty cup-closed diff-closed preBoolean finite V41() subset-closed binary_complete set
F₁() is set
F₂() is set
C2 is set
C1 is finite set
bool C1 is non empty cup-closed diff-closed preBoolean finite V41() subset-closed binary_complete set
x1 is set
x1 is set
y1 is set
x1 is set
y1 is set
x2 is set
x1 is finite set
y1 is set
x2 is set
C1 is non empty subset-closed binary_complete set
C2 is Element of C1
C1 is set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
{} C1 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered Element of bool C1
union ({} C1) is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal set
C2 is set
C1 is set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
{} C1 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered Element of bool C1
C2 is set
C1 is set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
C2 is set
x1 is set
C2 \/ x1 is set
{C2,x1} is non empty finite set
union {C2,x1} is set
C1 is non empty set
the Element of C1 is Element of C1
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
x1 is finite Element of bool C1
union x1 is set
y1 is set
x2 is set
union x2 is set
y2 is set
y2 is set
y2 \/ y1 is set
x is set
{y1} is non empty trivial finite 1 -element set
x2 \/ {y1} is non empty set
union (x2 \/ {y1}) is set
union {y1} is set
(union x2) \/ (union {y1}) is set
(union x2) \/ y1 is set
C1 is set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
C2 is set
x1 is set
C2 /\ x1 is set
{C2,x1} is non empty finite set
y1 is set
C1 is non empty set
the Element of C1 is Element of C1
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
x1 is finite Element of bool C1
y1 is set
x2 is set
y2 is set
y2 is set
y2 /\ y1 is set
x is set
{y1} is non empty trivial finite 1 -element set
x2 \/ {y1} is non empty set
y is set
y1 is set
C1 is set
{C1} is non empty trivial finite 1 -element set
bool {C1} is non empty cup-closed diff-closed preBoolean finite V41() subset-closed binary_complete set
x1 is trivial finite Element of bool {C1}
union x1 is set
union {C1} is set
y1 is set
x1 is trivial finite Element of bool {C1}
y1 is set
C1 is set
C2 is set
C1 \/ C2 is set
{C1,C2,(C1 \/ C2)} is non empty finite set
union {C1,C2,(C1 \/ C2)} is set
{C1,C2} is non empty finite set
{(C1 \/ C2)} is non empty trivial finite 1 -element set
{C1,C2} \/ {(C1 \/ C2)} is non empty finite set
union ({C1,C2} \/ {(C1 \/ C2)}) is set
union {C1,C2} is set
union {(C1 \/ C2)} is set
(union {C1,C2}) \/ (union {(C1 \/ C2)}) is set
(C1 \/ C2) \/ (union {(C1 \/ C2)}) is set
(C1 \/ C2) \/ (C1 \/ C2) is set
C1 is set
C2 is set
C1 \/ C2 is set
{C1,C2,(C1 \/ C2)} is non empty finite set
bool {C1,C2,(C1 \/ C2)} is non empty cup-closed diff-closed preBoolean finite V41() subset-closed binary_complete set
y1 is finite Element of bool {C1,C2,(C1 \/ C2)}
union y1 is set
x2 is set
union {C1,C2,(C1 \/ C2)} is set
C1 is set
C2 is set
C1 /\ C2 is set
{C1,C2,(C1 /\ C2)} is non empty finite set
bool {C1,C2,(C1 /\ C2)} is non empty cup-closed diff-closed preBoolean finite V41() subset-closed binary_complete set
x1 is finite Element of bool {C1,C2,(C1 /\ C2)}
y1 is set
x2 is set
C1 is non empty set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
the Element of C1 is Element of C1
{ the Element of C1} is non empty trivial finite 1 -element set
C1 is set
Fin C1 is non empty cup-closed diff-closed preBoolean set
C2 is set
x1 is set
C2 \/ x1 is set
y1 is set
x1 is set
y1 is set
C2 is set
x2 is set
x1 /\ y1 is set
C1 is set
Fin C1 is non empty cup-closed diff-closed preBoolean set
C1 is non empty subset-closed set
C2 is Element of C1
Fin C2 is non empty cup-closed diff-closed preBoolean () () set
x1 is set
C1 is non empty subset-closed set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
the Element of C1 is Element of C1
Fin the Element of C1 is non empty cup-closed diff-closed preBoolean () () set
x1 is Element of bool C1
C1 is non empty subset-closed set
C2 is Element of C1
Fin C2 is non empty cup-closed diff-closed preBoolean () () set
bool C1 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
x1 is set
C1 is non empty set
union C1 is set
C2 is set
the Element of C1 is Element of C1
y1 is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
y1 + 1 is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
x2 is set
card x2 is V8() V9() V10() cardinal set
y2 is non empty set
the Element of y2 is Element of y2
{ the Element of y2} is non empty trivial finite 1 -element set
x2 \ { the Element of y2} is Element of bool x2
bool x2 is non empty cup-closed diff-closed preBoolean subset-closed binary_complete set
y is set
(y1 + 1) - 1 is V15() V16() V17() Element of REAL
card { the Element of y2} is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
card (x2 \ { the Element of y2}) is V8() V9() V10() cardinal set
b is set
b \/ y is set
z2 is set
z1 is set
0 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered Element of NAT
y1 is set
card y1 is V8() V9() V10() cardinal set
card C2 is V8() V9() V10() cardinal set
y1 is finite set
card y1 is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
C1 is set
C2 is set
x1 is set
C2 /\ x1 is set
C1 is non empty cap-closed subset-closed binary_complete set
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete set
C2 is non empty () Element of bool C1
union C2 is set
x1 is set
y1 is set
x1 \/ y1 is set
x2 is set
C1 is non empty cap-closed subset-closed binary_complete set
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete set
C2 is Element of bool C1
union C2 is set
the non empty cap-closed subset-closed binary_complete () set is non empty cap-closed subset-closed binary_complete () set
C1 is non empty () set
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is non empty () Element of bool C1
union C2 is set
C1 is non empty set
C2 is set
x1 is set
C2 \/ x1 is set
C2 is set
x1 is set
C2 /\ x1 is set
C1 is set
C2 is set
x1 is set
C2 /\ x1 is set
C2 \/ x1 is set
C2 \/ C2 is set
x1 \/ x1 is set
{C2,x1} is non empty finite set
y1 is set
{C2,x1} is non empty finite set
x2 is set
y1 /\ x2 is set
y1 \/ x2 is set
C1 is Relation-like Function-like set
proj1 C1 is set
bool (proj1 C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is set
x1 is set
C1 . C2 is set
C1 . x1 is set
{C2,x1} is non empty finite set
y1 is Element of bool (proj1 C1)
bool y1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is finite Element of bool y1
union x2 is set
union y1 is set
C2 \/ x1 is set
C1 .: y1 is set
union y1 is set
C2 \/ x1 is set
union (C1 .: y1) is set
C1 is Relation-like Function-like set
proj1 C1 is set
bool (proj1 C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is Element of bool (proj1 C1)
union C2 is set
C1 . (union C2) is set
C1 .: C2 is set
union (C1 .: C2) is set
C1 is Relation-like Function-like set
proj1 C1 is set
C2 is set
x1 is set
C2 \/ x1 is set
C1 . (C2 \/ x1) is set
C1 . C2 is set
C1 . x1 is set
(C1 . C2) \/ (C1 . x1) is set
{C2,x1} is non empty finite set
union {C2,x1} is set
C1 .: {C2,x1} is finite set
union (C1 .: {C2,x1}) is set
{(C1 . C2),(C1 . x1)} is non empty finite set
union {(C1 . C2),(C1 . x1)} is set
C1 is Relation-like Function-like set
C1 . {} is set
proj1 C1 is set
bool (proj1 C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C1 .: {} is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Element of C2
C1 --> x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
proj1 y1 is set
bool (proj1 y1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is Element of bool (proj1 y1)
union x2 is set
y1 . (union x2) is set
y1 .: x2 is set
union (y1 .: x2) is set
y2 is set
x is set
y1 . x is set
x2 is set
y2 is set
x2 /\ y2 is set
y1 . (x2 /\ y2) is set
y1 . x2 is set
y1 . y2 is set
(y1 . x2) /\ (y1 . y2) is set
C1 is non empty cap-closed subset-closed binary_complete () set
[:C1,C1:] is non empty Relation-like set
bool [:C1,C1:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
the Relation-like C1 -defined C1 -valued Function-like V34(C1,C1) () () () () Element of bool [:C1,C1:] is Relation-like C1 -defined C1 -valued Function-like V34(C1,C1) () () () () Element of bool [:C1,C1:]
proj1 the Relation-like C1 -defined C1 -valued Function-like V34(C1,C1) () () () () Element of bool [:C1,C1:] is set
x1 is Relation-like C1 -defined Function-like V30(C1) set
C1 is Relation-like Function-like set
C1 is Relation-like Function-like set
C1 is Relation-like Function-like set
C1 is () set
C2 is Relation-like C1 -defined Function-like V30(C1) set
proj1 C2 is set
C1 is cap-closed set
C2 is Relation-like C1 -defined Function-like V30(C1) set
proj1 C2 is set
C1 is Relation-like Function-like set
the non empty cap-closed subset-closed binary_complete () set is non empty cap-closed subset-closed binary_complete () set
the Relation-like the non empty cap-closed subset-closed binary_complete () set -defined Function-like V30( the non empty cap-closed subset-closed binary_complete () set ) () () () () () () () set is Relation-like the non empty cap-closed subset-closed binary_complete () set -defined Function-like V30( the non empty cap-closed subset-closed binary_complete () set ) () () () () () () () set
C1 is non empty cap-closed subset-closed binary_complete () set
the Relation-like C1 -defined Function-like V30(C1) () () () () () () () set is Relation-like C1 -defined Function-like V30(C1) () () () () () () () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C2,C1:] is non empty Relation-like set
bool [:C2,C1:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
the Relation-like C2 -defined C1 -valued Function-like V34(C2,C1) () () () () Element of bool [:C2,C1:] is Relation-like C2 -defined C1 -valued Function-like V34(C2,C1) () () () () Element of bool [:C2,C1:]
proj1 the Relation-like C2 -defined C1 -valued Function-like V34(C2,C1) () () () () Element of bool [:C2,C1:] is set
y1 is Relation-like C2 -defined Function-like V30(C2) () () () () () () () set
C1 is Relation-like Function-like () () () set
proj1 C1 is set
C1 is Relation-like Function-like () () () () () set
proj1 C1 is () set
C1 is set
Fin C1 is non empty cup-closed diff-closed preBoolean () () set
union (Fin C1) is set
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union (bool C1) is set
C2 is set
{C2} is non empty trivial finite 1 -element set
C1 is Relation-like Function-like () () () set
proj1 C1 is () set
C2 is set
C1 . C2 is set
Fin C2 is non empty cup-closed diff-closed preBoolean () () set
C1 .: (Fin C2) is set
union (C1 .: (Fin C2)) is set
x1 is non empty cap-closed subset-closed () set
y1 is Element of x1
C1 . y1 is set
(x1,y1) is non empty cup-closed diff-closed preBoolean () () Element of bool x1
bool x1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
(x1,(x1,y1)) is Element of x1
C1 . (x1,(x1,y1)) is set
C1 is Relation-like Function-like set
proj1 C1 is set
x1 is set
y1 is set
C1 . x1 is set
bool x1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b₁ where b₁ is Element of bool x1 : b₁ is finite } is set
x2 is set
bool x2 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is finite Element of bool x2
union y2 is set
x is set
y is Element of bool x1
x is set
y is Element of bool x1
union x2 is set
y2 is set
x is set
y is Element of bool x1
y2 is set
{y2} is non empty trivial finite 1 -element set
C2 is cap-closed subset-closed () set
y2 is set
x is Element of bool x1
C1 . (union x2) is set
C1 .: x2 is set
union (C1 .: x2) is set
y2 is set
x is set
C1 . x is set
y is set
C1 . y is set
b is Element of bool x1
C2 is () set
bool (proj1 C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Element of bool (proj1 C1)
union x1 is set
C1 . (union x1) is set
C1 .: x1 is set
union (C1 .: x1) is set
bool C2 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y1 is Element of bool C2
union y1 is set
y2 is set
C1 . y2 is set
x is set
C1 . x is set
x2 is set
y2 is set
y1 is Element of bool C2
union y1 is set
C1 . (union y1) is set
x is set
C1 . x is set
C1 is Relation-like Function-like set
proj1 C1 is set
x1 is Relation-like Function-like () () () () () set
proj1 x1 is cap-closed () set
y1 is set
x2 is set
C1 . y1 is set
x is set
x1 . x is set
bool x is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b₁ where b₁ is Element of bool x : x2 in C1 . b₁ } is set
y is non empty set
b is set
z2 is Element of bool x
C1 . z2 is set
b is set
z2 is set
z1 is set
b is set
z2 is set
b is non empty finite set
z2 is set
z is Element of bool x
C1 . z is set
z1 is Element of bool x
y is set
C1 . y is set
zz is Element of bool x
C1 . zz is set
z is finite Element of bool x
zz is set
C1 . zz is set
y \/ zz is set
y /\ zz is set
C1 . (y /\ zz) is set
(C1 . y) /\ (C1 . zz) is set
y is Element of bool x
C1 . y is set
C2 is cap-closed subset-closed () set
x1 is set
y1 is set
C1 . x1 is set
x2 is set
C1 . x2 is set
x1 is set
y1 is set
x1 /\ y1 is set
C1 . (x1 /\ y1) is set
C1 . x1 is set
C1 . y1 is set
(C1 . x1) /\ (C1 . y1) is set
x2 is set
x1 \/ y1 is set
C1 . (x1 \/ y1) is set
y2 is set
C1 . y2 is set
C1 is Relation-like Function-like set
proj1 C1 is set
bool (proj1 C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
C1 . x1 is set
x2 is set
C1 . x2 is set
C2 is cap-closed subset-closed () set
C1 . {} is set
C1 .: {} is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
union (C1 .: {}) is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal set
y2 is non empty set
{ {b₁} where b₁ is Element of y2 : verum } is set
x is set
y is set
b is Element of y2
{b} is non empty trivial finite 1 -element set
y is set
b is Element of y2
{b} is non empty trivial finite 1 -element set
union x is set
y is Element of bool (proj1 C1)
union y is set
b is set
{b} is non empty trivial finite 1 -element set
C1 . y2 is set
C1 . (union y) is set
C1 .: y is set
union (C1 .: y) is set
b is set
z2 is set
C1 . z2 is set
z1 is Element of y2
{z1} is non empty trivial finite 1 -element set
z is set
y is set
{y} is non empty trivial finite 1 -element set
C1 . {y} is set
zz is set
C1 . zz is set
x1 is set
y1 is set
C1 . x1 is set
x2 is set
{x2} is non empty trivial finite 1 -element set
C1 . {x2} is set
y2 is set
x is set
C1 . x is set
y is set
C1 . y is set
x1 is Element of bool (proj1 C1)
union x1 is set
C1 . (union x1) is set
C1 .: x1 is set
union (C1 .: x1) is set
y1 is set
x2 is set
{x2} is non empty trivial finite 1 -element set
C1 . {x2} is set
y2 is set
C1 . y2 is set
y1 is set
x2 is set
C1 . x2 is set
C1 is Relation-like Function-like set
proj1 C1 is set
proj2 C1 is set
union (proj2 C1) is set
[:(proj1 C1),(union (proj2 C1)):] is Relation-like set
C2 is set
x1 is set
y1 is finite set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite V41() 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
y1 is finite set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite V41() 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
C2 is set
x1 is set
y1 is set
x2 is finite set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite V41() 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
C1 . x2 is set
x2 is finite set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite V41() 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
C1 . x2 is set
C1 is non empty set
C2 is non empty set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
(x1) is set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is set
proj1 x1 is set
x2 is finite set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite V41() 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
x1 . x2 is set
proj2 x1 is set
C1 is Relation-like Function-like set
(C1) is set
C2 is set
proj1 C1 is set
x1 is finite set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite V41() 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
C1 . x1 is set
C1 is Relation-like Function-like set
(C1) is Relation-like set
proj1 C1 is set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
C1 . C2 is set
y1 is finite set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite V41() 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
C1 is Relation-like Function-like () set
proj1 C1 is set
(C1) is Relation-like set
x1 is set
C2 is set
y1 is set
[C2,y1] is V31() set
{C2,y1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,y1},{C2}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
C1 . C2 is set
C1 . x1 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{{y1,y2},{y1}} is non empty finite V41() set
{x2,y2} is non empty finite set
x1 . y1 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x2 is Element of C1
y1 \/ x2 is set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
{y2,x} is non empty finite set
proj1 x1 is set
y is finite Element of C1
[y,y2] is V31() set
{y,y2} is non empty finite set
{y} is non empty trivial finite V41() 1 -element set
{{y,y2},{y}} is non empty finite V41() set
[y,x] is V31() set
{y,x} is non empty finite set
{{y,x},{y}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
proj1 x1 is () set
proj1 y1 is () set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
proj1 y2 is () set
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is finite Element of C1
y2 . x2 is Element of C2
x . x2 is Element of C2
y is set
[x2,y] is V31() set
{x2,y} is non empty finite set
{x2} is non empty trivial finite V41() 1 -element set
{{x2,y},{x2}} is non empty finite V41() set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
proj1 x is () set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is Element of C1
(C1,x2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 .: (C1,x2) is set
x .: (C1,x2) is set
y is set
proj1 y2 is () set
b is set
y2 . b is set
x . b is set
x2 is Element of C1
(C1,x2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,x2) is set
y1 .: (C1,x2) is set
x1 . x2 is Element of C2
union (x1 .: (C1,x2)) is set
y1 . x2 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y1 is Relation-like Function-like set
proj1 y1 is set
proj2 y1 is set
x2 is set
y2 is set
y1 . y2 is set
x is Element of C1
(C1,x) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 .: (C1,x) is set
y is set
z2 is set
[z2,y] is V31() set
{z2,y} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,y},{z2}} is non empty finite V41() set
b is set
z1 is set
[z1,b] is V31() set
{z1,b} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,b},{z1}} is non empty finite V41() set
z is finite Element of C1
y is finite Element of C1
z \/ y is finite set
zz is finite Element of C1
[zz,b] is V31() set
{zz,b} is non empty finite set
{zz} is non empty trivial finite V41() 1 -element set
{{zz,b},{zz}} is non empty finite V41() set
[zz,y] is V31() set
{zz,y} is non empty finite set
{{zz,y},{zz}} is non empty finite V41() set
{y,b} is non empty finite set
x2 is set
y2 is set
y1 . x2 is set
Fin x2 is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin x2) is set
x is set
[x,y2] is V31() set
{x,y2} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y2},{x}} is non empty finite V41() set
y1 . x is set
Fin x is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin x) is set
y is set
Fin y is non empty cup-closed diff-closed preBoolean () () set
y1 . y is set
x2 is set
y2 is set
y1 . x2 is set
y1 . y2 is set
x is Element of C1
(C1,x) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y is Element of C1
(C1,y) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,x) is set
x1 .: (C1,y) is set
y1 . x is set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
[y2,x] `1 is set
y is finite Element of C1
Fin y2 is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin y2) is set
x2 . y is Element of C2
y is finite Element of C1
x2 . y is Element of C2
(C1,y) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 .: (C1,y) is set
b is set
[b,x] is V31() set
{b,x} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,x},{b}} is non empty finite V41() set
y2 is Element of C1
x2 . y2 is Element of C2
(C1,y2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 .: (C1,y2) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x1 . y1 is Element of C2
(C1,y1) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
(C1,C2,x1) .: (C1,y1) is set
y2 is set
proj1 x1 is () set
y2 `1 is set
x is finite set
y is set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite V41() 1 -element set
{{x,y},{x}} is non empty finite V41() set
x1 . x is set
y2 is finite Element of C1
x is finite Element of C1
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite V41() 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite V41() 1 -element set
{{x,y},{x}} is non empty finite V41() set
y2 is finite Element of C1
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite V41() 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{{y2,y},{y2}} is non empty finite V41() set
{x,y} is non empty finite set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y2 . y1 is Element of C2
C1 is Relation-like Function-like set
proj1 C1 is set
Union C1 is set
[:(proj1 C1),(Union C1):] is Relation-like set
C2 is set
x1 is set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
C2 is set
x1 is set
y1 is set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
C1 . x2 is set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
C1 . x2 is set
C1 is Relation-like Function-like set
(C1) is set
proj1 C1 is set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
C1 . C2 is set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
y2 is set
C1 . y2 is set
y1 is set
C1 . y1 is set
C1 is non empty set
C2 is non empty set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
(x1) is set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is set
proj1 x1 is set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
x1 . x2 is set
proj2 x1 is set
C1 is Relation-like Function-like set
(C1) is set
C2 is set
proj1 C1 is set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
C1 . x1 is set
C1 is Relation-like Function-like () () () set
proj1 C1 is () set
(C1) is Relation-like set
(C1) is Relation-like set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
C1 . y1 is set
y2 is set
C1 . y2 is set
C1 is Relation-like Function-like () () () set
proj1 C1 is () set
(C1) is Relation-like set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
C1 . C2 is set
y1 is set
C1 . y1 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x1 is set
y1 is set
x2 is set
y1 \/ x2 is set
x is Element of C1
x1 . x2 is set
x1 . x is Element of C2
y is set
[y1,y] is V31() set
{y1,y} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y},{y1}} is non empty finite V41() set
b is set
[x2,b] is V31() set
{x2,b} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,b},{x2}} is non empty finite V41() set
{y,b} is non empty finite set
x1 . y1 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x1 is set
y1 is set
x2 is set
y1 \/ x2 is set
y1 /\ x2 is set
x is Element of C1
y is set
[y1,y] is V31() set
{y1,y} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y},{y1}} is non empty finite V41() set
[x2,y] is V31() set
{x2,y} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y},{x2}} is non empty finite V41() set
x1 . y1 is set
x1 . x2 is set
(x1 . y1) /\ (x1 . x2) is set
x1 . x is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is Element of C1
x1 . x2 is Element of C2
y1 . x2 is Element of C2
proj1 x1 is cap-closed () set
y2 is set
x is set
x1 . x is set
b is set
y is Element of C1
x1 . b is set
[y,y2] is V31() set
{y,y2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y2},{y}} is non empty finite V41() set
y1 . y is Element of C2
proj1 y1 is cap-closed () set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
proj1 x1 is cap-closed () set
proj1 y1 is cap-closed () set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
proj1 x is cap-closed () set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is Element of C1
(C1,x2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 .: (C1,x2) is set
x .: (C1,x2) is set
y is set
proj1 y2 is cap-closed () set
b is set
y2 . b is set
x . b is set
x2 is Element of C1
(C1,x2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,x2) is set
y1 .: (C1,x2) is set
x1 . x2 is Element of C2
union (x1 .: (C1,x2)) is set
y1 . x2 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y1 is Relation-like Function-like set
proj1 y1 is set
x2 is set
y2 is set
y1 . x2 is set
Fin x2 is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin x2) is set
y is set
[y,y2] is V31() set
{y,y2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y2},{y}} is non empty finite V41() set
y1 . y is set
Fin y is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin y) is set
b is set
Fin b is non empty cup-closed diff-closed preBoolean () () set
y1 . b is set
z2 is set
y1 . z2 is set
x is Element of C1
Fin z2 is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin z2) is set
z1 is set
[z1,y2] is V31() set
{z1,y2} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,y2},{z1}} is non empty finite V41() set
(C1,x) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
b \/ z1 is set
proj2 y1 is set
x2 is set
y2 is set
y1 . y2 is set
x is Element of C1
(C1,x) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,x) is set
y is set
z2 is set
[z2,y] is V31() set
{z2,y} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,y},{z2}} is non empty finite V41() set
b is set
z1 is set
[z1,b] is V31() set
{z1,b} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,b},{z1}} is non empty finite V41() set
z2 \/ z1 is set
{y,b} is non empty finite set
x2 is set
y2 is set
y1 . x2 is set
y1 . y2 is set
x is Element of C1
(C1,x) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
y is Element of C1
(C1,y) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,x) is set
x1 .: (C1,y) is set
y1 . x is set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
[y2,x] `1 is set
y is finite Element of C1
Fin y2 is non empty cup-closed diff-closed preBoolean () () set
x1 .: (Fin y2) is set
b is set
proj1 x2 is cap-closed () set
x2 . b is set
z2 is Element of C1
(C1,z2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,z2) is set
z1 is set
[z1,x] is V31() set
{z1,x} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,x},{z1}} is non empty finite V41() set
z1 \/ y is set
x2 . y is Element of C2
x2 . y2 is set
y is set
[y,x] is V31() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V41() set
b is Element of C1
(C1,b) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
z2 is finite Element of C1
(C1,z2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,z2) is set
x2 . z2 is Element of C2
y2 is Element of C1
x2 . y2 is Element of C2
(C1,y2) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
x1 .: (C1,y2) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x1 . y1 is Element of C2
(C1,y1) is non empty cup-closed diff-closed preBoolean () () Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
(C1,C2,x1) .: (C1,y1) is set
proj1 x1 is cap-closed () set
y2 is set
x is set
y is set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
x1 . x is set
y2 `1 is set
y2 is Element of C1
x is Element of C1
y2 \/ x is set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
b is set
[x,b] is V31() set
{x,b} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,b},{x}} is non empty finite V41() set
{y,b} is non empty finite set
z2 is Element of C1
z1 is Element of C1
z2 \/ z1 is set
z is set
[z2,z] is V31() set
{z2,z} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,z},{z2}} is non empty finite V41() set
[z1,z] is V31() set
{z1,z} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,z},{z1}} is non empty finite V41() set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y2 . y1 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x1 . y1 is Element of C2
x2 is set
proj1 x1 is cap-closed () set
y2 is set
x1 . y2 is set
x is Element of C1
b is set
y is Element of C1
x1 . b is set
[y,x2] is V31() set
{y,x2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x2},{y}} is non empty finite V41() set
y2 is Element of C1
[y2,x2] is V31() set
{y2,x2} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x2},{y2}} is non empty finite V41() set
x1 . y2 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
y1 is Element of C1
x2 is Element of C1
y1 \/ x2 is set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
y1 is set
y1 `1 is set
x2 is Element of C1
y2 is Element of C1
x2 \/ y2 is set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
{x,y} is non empty finite set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is finite Element of C1
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite V41() 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is Element of C1
x is Element of C1
y2 \/ x is set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
x2 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
b is set
[x,b] is V31() set
{x,b} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,b},{x}} is non empty finite V41() set
{y,b} is non empty finite set
{y1} is non empty trivial finite 1 -element set
y2 is Element of C1
x is Element of C1
y2 \/ x is set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
y2 is set
y2 `1 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Element of C1
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
{y1} is non empty trivial finite 1 -element set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is Element of C1
x2 . y2 is Element of C2
x is set
y is Element of C1
[y,x] is V31() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V41() set
x is non empty set
the Element of x is Element of x
b is Element of C1
[b, the Element of x] is V31() set
{b, the Element of x} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b, the Element of x},{b}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
bool (C1,C2,x1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like C1 -defined union C2 -valued Element of bool (C1,C2,x1)
x2 is Element of C1
y2 is Element of C1
x2 \/ y2 is set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
x2 is set
proj1 x1 is cap-closed () set
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
x1 . y2 is set
x2 `1 is set
x2 is Element of C1
y2 is Element of C1
x2 \/ y2 is set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
{x,y} is non empty finite set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
union x1 is set
x2 is Element of C1
y2 is Element of C1
x2 \/ y2 is set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
b is set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
z2 is set
b \/ z2 is set
{x,y} is non empty finite set
z1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,z1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is Element of C1
y2 is Element of C1
x2 \/ y2 is set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
y is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
b is set
y \/ b is set
z2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,z2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y2 is set
y2 \/ y2 is set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x is cap-closed () set
y is set
b is set
[y,b] is V31() set
{y,b} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,b},{y}} is non empty finite V41() set
x . y is set
x2 `1 is set
x2 is set
y2 is set
y2 \/ y2 is set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
x2 is set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
the Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:] is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2, the Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y2 is set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is set
union x2 is set
y2 is set
x is set
y2 \/ x is set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
[:(C1),(union C2):] is Relation-like set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
proj1 x1 is cap-closed () set
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
x1 . y2 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
union (C1,C2) is set
(C1) is non empty cap-closed subset-closed Element of bool C1
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
[:(C1),(union C2):] is Relation-like set
x1 is set
y1 is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
Web C2 is Relation-like union C2 -defined union C2 -valued V30( union C2) V57() V59() Element of bool [:(union C2),(union C2):]
[:(union C2),(union C2):] is Relation-like set
bool [:(union C2),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is finite Element of C1
y1 is finite Element of C1
x1 \/ y1 is finite set
x2 is set
[x1,x2] is V31() set
{x1,x2} is non empty finite set
{x1} is non empty trivial finite V41() 1 -element set
{{x1,x2},{x1}} is non empty finite V41() set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite V41() 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
[[x1,x2],[y1,y2]] is V31() set
{[x1,x2],[y1,y2]} is non empty Relation-like finite set
{[x1,x2]} is non empty trivial Relation-like finite 1 -element set
{{[x1,x2],[y1,y2]},{[x1,x2]}} is non empty finite V41() set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y is Element of C1
b is Element of C1
y \/ b is set
z2 is set
[y,z2] is V31() set
{y,z2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z2},{y}} is non empty finite V41() set
x is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
z1 is set
[b,z1] is V31() set
{b,z1} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,z1},{b}} is non empty finite V41() set
{z2,z1} is non empty finite set
{y2} is non empty trivial finite 1 -element set
y is Element of C1
b is Element of C1
y \/ b is set
z2 is set
[y,z2] is V31() set
{y,z2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z2},{y}} is non empty finite V41() set
[b,z2] is V31() set
{b,z2} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,z2},{b}} is non empty finite V41() set
y is set
y `1 is set
y is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,y) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
union C2 is set
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x1 is cap-closed () set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
x1 . y1 is set
y2 is set
{y2} is non empty trivial finite 1 -element set
x1 . {y2} is set
x is set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
y1 is set
x2 is set
x1 . y1 is set
y2 is set
x1 . y2 is set
x is set
x1 . x is set
[y2,x2] is V31() set
{y2,x2} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x2},{y2}} is non empty finite V41() set
x is set
{x} is non empty trivial finite 1 -element set
y is set
{y} is non empty trivial finite 1 -element set
x1 . {y} is set
b is set
x1 . b is set
C1 is Relation-like Function-like set
(C1) is Relation-like set
C2 is set
x1 is set
y1 is set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[{x2},y2] is V31() set
{{x2},y2} is non empty finite set
{{x2}} is non empty trivial finite V41() 1 -element set
{{{x2},y2},{{x2}}} is non empty finite V41() set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[{x2},y2] is V31() set
{{x2},y2} is non empty finite set
{{x2}} is non empty trivial finite V41() 1 -element set
{{{x2},y2},{{x2}}} is non empty finite V41() set
proj1 C1 is set
proj2 C1 is set
union (proj1 C1) is set
union (proj2 C1) is set
[:(union (proj1 C1)),(union (proj2 C1)):] is Relation-like set
y1 is set
x2 is set
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
[{y2},x] is V31() set
{{y2},x} is non empty finite set
{{y2}} is non empty trivial finite V41() 1 -element set
{{{y2},x},{{y2}}} is non empty finite V41() set
C1 . {y2} is set
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
[{y2},x] is V31() set
{{y2},x} is non empty finite set
{{y2}} is non empty trivial finite V41() 1 -element set
{{{y2},x},{{y2}}} is non empty finite V41() set
C1 is Relation-like Function-like set
(C1) is set
(C1) is Relation-like set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
[{C2},x1] is V31() set
{{C2},x1} is non empty finite set
{{C2}} is non empty trivial finite V41() 1 -element set
{{{C2},x1},{{C2}}} is non empty finite V41() set
y1 is set
x2 is set
[y1,x2] is V31() set
{y1,x2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x2},{y1}} is non empty finite V41() set
[{y1},x2] is V31() set
{{y1},x2} is non empty finite set
{{y1}} is non empty trivial finite V41() 1 -element set
{{{y1},x2},{{y1}}} is non empty finite V41() set
C1 is Relation-like Function-like set
C1 . {} is set
proj1 C1 is set
(C1) is set
C2 is set
{C2} is non empty trivial finite 1 -element set
x1 is set
C1 . {C2} is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{{C2,x1},{C2}} is non empty finite V41() set
[{C2},x1] is V31() set
{{C2},x1} is non empty finite set
{{C2}} is non empty trivial finite V41() 1 -element set
{{{C2},x1},{{C2}}} is non empty finite V41() set
(C1) is Relation-like set
x2 is set
C1 . x2 is set
x2 is set
C1 . x2 is set
C1 is Relation-like Function-like set
(C1) is set
proj1 C1 is set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
C1 . {C2} is set
[{C2},x1] is V31() set
{{C2},x1} is non empty finite set
{{C2}} is non empty trivial finite V41() 1 -element set
{{{C2},x1},{{C2}}} is non empty finite V41() set
(C1) is Relation-like set
C1 is non empty set
C2 is non empty set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) Element of bool [:C1,C2:]
(x1) is set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is set
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[{x2},y2] is V31() set
{{x2},y2} is non empty finite set
{{x2}} is non empty trivial finite V41() 1 -element set
{{{x2},y2},{{x2}}} is non empty finite V41() set
proj1 x1 is set
C1 is Relation-like Function-like set
(C1) is set
C2 is set
(C1) is Relation-like set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
[{x1},y1] is V31() set
{{x1},y1} is non empty finite set
{{x1}} is non empty trivial finite V41() 1 -element set
{{{x1},y1},{{x1}}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
x2 is set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x1 is set
y1 is set
x2 is set
{y1,x2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
y2 is Element of C1
x1 . {x2} is set
x1 . y2 is Element of C2
x is set
[y1,x] is V31() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x},{y1}} is non empty finite V41() set
y is set
[x2,y] is V31() set
{x2,y} is non empty finite set
{{x2,y},{x2}} is non empty finite V41() set
{x,y} is non empty finite set
x1 . {y1} is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is set
x2 is set
{y1,x2} is non empty finite set
x is set
[y1,x] is V31() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,x},{y1}} is non empty finite V41() set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
{y1} \/ {x2} is non empty finite set
[{y1},x] is V31() set
{{y1},x} is non empty finite set
{{y1}} is non empty trivial finite V41() 1 -element set
{{{y1},x},{{y1}}} is non empty finite V41() set
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[{x2},x] is V31() set
{{x2},x} is non empty finite set
{{x2}} is non empty trivial finite V41() 1 -element set
{{{x2},x},{{x2}}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
(C1,C2,x1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
(C1,C2,y1) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
x2 is set
y2 is set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
x is set
{x} is non empty trivial finite 1 -element set
[x,y2] is V31() set
{x,y2} is non empty finite set
{{x,y2},{x}} is non empty finite V41() set
x is set
{x} is non empty trivial finite 1 -element set
[x,y2] is V31() set
{x,y2} is non empty finite set
{{x,y2},{x}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
y1 is Relation-like Function-like set
proj1 y1 is set
x2 is set
y2 is set
y1 . x2 is set
x1 .: x2 is set
y is set
[y,y2] is V31() set
{y,y2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y2},{y}} is non empty finite V41() set
b is set
{b} is non empty trivial finite 1 -element set
y1 . {b} is set
x1 .: {b} is set
z2 is set
y1 . z2 is set
x is Element of C1
x1 .: z2 is set
z1 is set
[z1,y2] is V31() set
{z1,y2} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,y2},{z1}} is non empty finite V41() set
{b,z1} is non empty finite set
proj2 y1 is set
x2 is set
y2 is set
y1 . y2 is set
x is Element of C1
x1 .: x is set
y is set
z2 is set
[z2,y] is V31() set
{z2,y} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,y},{z2}} is non empty finite V41() set
b is set
z1 is set
[z1,b] is V31() set
{z1,b} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,b},{z1}} is non empty finite V41() set
{z2,z1} is non empty finite set
{y,b} is non empty finite set
x2 is set
y2 is set
y1 . x2 is set
y1 . y2 is set
x is Element of C1
y1 . x is set
x1 .: x is set
y is Element of C1
x1 .: y is set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
y2 is set
x is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
y is set
b is Element of C1
x2 . b is Element of C2
x1 .: b is set
x2 . {} is set
x2 . {y2} is set
x1 .: {y2} is set
y is set
[y,x] is V31() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V41() set
y2 is Element of C1
x2 . y2 is Element of C2
x1 .: y2 is set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
y1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Element of C1
x1 . y1 is Element of C2
(C1,C2,x1) .: y1 is set
y2 is set
x is set
{y2,x} is non empty finite set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
b is set
[x,b] is V31() set
{x,b} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,b},{x}} is non empty finite V41() set
{y,b} is non empty finite set
z2 is set
z1 is set
{z2,z1} is non empty finite set
z is set
[z2,z] is V31() set
{z2,z} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,z},{z2}} is non empty finite V41() set
[z1,z] is V31() set
{z1,z} is non empty finite set
{z1} is non empty trivial finite 1 -element set
{{z1,z},{z1}} is non empty finite V41() set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
y2 . y1 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
y1 is set
x2 is set
{y1,x2} is non empty finite set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
{y2,x} is non empty finite set
y is set
b is set
{y,b} is non empty finite set
z2 is set
[y,z2] is V31() set
{y,z2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z2},{y}} is non empty finite V41() set
[b,z2] is V31() set
{b,z2} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,z2},{b}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y2 is set
x is set
{y2,x} is non empty finite set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
x2 is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
b is set
[x,b] is V31() set
{x,b} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,b},{x}} is non empty finite V41() set
{y,b} is non empty finite set
{y1} is non empty trivial finite 1 -element set
y2 is set
x is set
{y2,x} is non empty finite set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
{y1} is non empty trivial finite 1 -element set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x is Element of C1
y2 . x is Element of C2
y2 . {x1} is set
y is set
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
b is Element of C1
[b,y] is V31() set
{b,y} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,y},{b}} is non empty finite V41() set
z2 is set
{z2} is non empty trivial finite 1 -element set
[z2,y] is V31() set
{z2,y} is non empty finite set
{{z2,y},{z2}} is non empty finite V41() set
x2 is Element of C1
proj1 y2 is cap-closed () set
y2 . x2 is Element of C2
y is non empty set
the Element of y is Element of y
(C1,C2,y2) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
z2 is Element of C1
[z2, the Element of y] is V31() set
{z2, the Element of y} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2, the Element of y},{z2}} is non empty finite V41() set
z1 is set
{z1} is non empty trivial finite 1 -element set
[z1, the Element of y] is V31() set
{z1, the Element of y} is non empty finite set
{{z1, the Element of y},{z1}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C1 is set
union C2 is set
x1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
bool (C1,C2,x1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
y1 is Relation-like union C1 -defined union C2 -valued Element of bool (C1,C2,x1)
x2 is set
y2 is set
{x2,y2} is non empty finite set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
x2 is set
y2 is set
{x2,y2} is non empty finite set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
{x,y} is non empty finite set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
union x1 is set
x2 is set
y2 is set
{x2,y2} is non empty finite set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
b is set
y is set
[y2,y] is V31() set
{y2,y} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,y},{y2}} is non empty finite V41() set
z2 is set
b \/ z2 is set
{x,y} is non empty finite set
z1 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,z1) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y2 is set
{x2,y2} is non empty finite set
x is set
[x2,x] is V31() set
{x2,x} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x},{x2}} is non empty finite V41() set
y is set
[y2,x] is V31() set
{y2,x} is non empty finite set
{y2} is non empty trivial finite 1 -element set
{{y2,x},{y2}} is non empty finite V41() set
b is set
y \/ b is set
z2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,z2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
x2 is set
y2 is set
y2 \/ y2 is set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
the Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:] is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2, the Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is set
y2 is set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
x2 is set
union x2 is set
y2 is set
x is set
y2 \/ x is set
y2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,y2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
union (C1,C2) is set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
x1 is set
y1 is set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{[x1,y1]} is non empty trivial Relation-like finite 1 -element set
x2 is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x2) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C1 is set
Web C1 is Relation-like union C1 -defined union C1 -valued V30( union C1) V57() V59() Element of bool [:(union C1),(union C1):]
[:(union C1),(union C1):] is Relation-like set
bool [:(union C1),(union C1):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
union C2 is set
Web C2 is Relation-like union C2 -defined union C2 -valued V30( union C2) V57() V59() Element of bool [:(union C2),(union C2):]
[:(union C2),(union C2):] is Relation-like set
bool [:(union C2),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
x2 is set
[x1,x2] is V31() set
{x1,x2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,x2},{x1}} is non empty finite V41() set
y1 is set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
[[x1,x2],[y1,y2]] is V31() set
{[x1,x2],[y1,y2]} is non empty Relation-like finite set
{[x1,x2]} is non empty trivial Relation-like finite 1 -element set
{{[x1,x2],[y1,y2]},{[x1,x2]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[:C1,C2:] is non empty Relation-like set
bool [:C1,C2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () () () Element of bool [:C1,C2:]
(C1,C2,x) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
[:(union C1),(union C2):] is Relation-like set
bool [:(union C1),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
[{x1},x2] is V31() set
{{x1},x2} is non empty finite set
{{x1}} is non empty trivial finite V41() 1 -element set
{{{x1},x2},{{x1}}} is non empty finite V41() set
(C1,C2,x) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
[:C1,(union C2):] is Relation-like set
bool [:C1,(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
proj1 x is cap-closed () set
[{y1},y2] is V31() set
{{y1},y2} is non empty finite set
{{y1}} is non empty trivial finite V41() 1 -element set
{{{y1},y2},{{y1}}} is non empty finite V41() set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{[{x1},x2],[{y1},y2]} is non empty Relation-like finite set
[[{x1},x2],[{y1},y2]] is V31() set
{[{x1},x2]} is non empty trivial Relation-like finite 1 -element set
{{[{x1},x2],[{y1},y2]},{[{x1},x2]}} is non empty finite V41() set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{x1} \/ {y1} is non empty finite set
x is Element of C1
y is Element of C1
x \/ y is set
[x,x2] is V31() set
{x,x2} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x2},{x}} is non empty finite V41() set
[y,y2] is V31() set
{y,y2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y2},{y}} is non empty finite V41() set
[[x,x2],[y,y2]] is V31() set
{[x,x2],[y,y2]} is non empty Relation-like finite set
{[x,x2]} is non empty trivial Relation-like finite 1 -element set
{{[x,x2],[y,y2]},{[x,x2]}} is non empty finite V41() set
b is Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) () () () () () Element of bool [:C1,C2:]
(C1,C2,b) is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]
z2 is set
z1 is set
[z2,z1] is V31() set
{z2,z1} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,z1},{z2}} is non empty finite V41() set
(C1,C2,b) is Relation-like union C1 -defined union C2 -valued Element of bool [:(union C1),(union C2):]
z2 is set
z1 is set
[z2,z1] is V31() set
{z2,z1} is non empty finite set
{z2} is non empty trivial finite 1 -element set
{{z2,z1},{z2}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
x1 is Element of bool (union C1)
x1 is Element of C1
C2 /\ x1 is set
y1 is Element of bool (union C1)
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is Element of bool (union C1)
x1 is Element of C1
C2 /\ x1 is Element of bool (union C1)
y1 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
{y1} is non empty trivial finite V41() 1 -element set
x1 is set
x2 is Element of bool (union C1)
y1 is set
x is Element of C1
x2 /\ x is Element of bool (union C1)
y is set
{y} is non empty trivial finite 1 -element set
y1 /\ x is set
x1 /\ x is set
y2 is Element of bool (union C1)
y2 /\ x is Element of bool (union C1)
b is set
{b} is non empty trivial finite 1 -element set
x1 is set
union x1 is set
y1 is set
y1 \/ y1 is set
x2 is Element of bool (union C1)
union (bool (union C1)) is set
y1 is Element of bool (union C1)
x2 is Element of C1
y1 /\ x2 is Element of bool (union C1)
y2 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered set
{y2} is non empty trivial finite V41() 1 -element set
y1 is Element of bool (union C1)
x2 is Element of C1
y1 /\ x2 is Element of bool (union C1)
y2 is non empty set
the Element of y2 is Element of y2
y is set
b is set
{b} is non empty trivial finite 1 -element set
z2 is set
z1 is set
z is set
z1 \/ z is set
y is Element of bool (union C1)
y /\ x2 is Element of bool (union C1)
zz is set
{zz} is non empty trivial finite 1 -element set
y1 is Element of bool (union C1)
x2 is Element of C1
y1 /\ x2 is Element of bool (union C1)
y1 is Element of bool (union C1)
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
union (C1) is set
C2 is set
x1 is set
C2 is set
{C2} is non empty trivial finite 1 -element set
x1 is Element of C1
{C2} /\ x1 is finite set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
x1 is set
{C2,x1} is non empty finite set
{C2,x1} /\ {C2,x1} is finite set
y1 is set
{y1} is non empty trivial finite 1 -element set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
(C1) is non empty cap-closed subset-closed binary_complete () set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
x1 is set
{C2,x1} is non empty finite set
y1 is Element of C1
x2 is set
{C2,x1} /\ y1 is finite set
y2 is set
{y2} is non empty trivial finite 1 -element set
x is set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
Web (C1) is Relation-like union (C1) -defined union (C1) -valued V30( union (C1)) V57() V59() Element of bool [:(union (C1)),(union (C1)):]
union (C1) is set
[:(union (C1)),(union (C1)):] is Relation-like set
bool [:(union (C1)),(union (C1)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
Web C1 is Relation-like union C1 -defined union C1 -valued V30( union C1) V57() V59() Element of bool [:(union C1),(union C1):]
[:(union C1),(union C1):] is Relation-like set
bool [:(union C1),(union C1):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is set
x1 is set
[C2,x1] is V31() set
{C2,x1} is non empty finite set
{C2} is non empty trivial finite 1 -element set
{{C2,x1},{C2}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
((C1)) is non empty cap-closed subset-closed binary_complete () set
union (C1) is set
bool (union (C1)) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union (C1)) : for b<sub>2</sub> being Element of (C1) ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
x1 is Element of bool (union (C1))
y1 is set
x2 is set
{y1,x2} is non empty finite set
x1 /\ {y1,x2} is finite Element of bool (union (C1))
y2 is set
{y2} is non empty trivial finite 1 -element set
{y1} is non empty trivial finite 1 -element set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union C1) : for b<sub>2</sub> being Element of C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
((C1)) is non empty cap-closed subset-closed binary_complete () set
union (C1) is set
bool (union (C1)) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union (C1)) : for b<sub>2</sub> being Element of (C1) ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
union ((C1)) is set
x1 is set
y1 is set
{x1,y1} is non empty finite set
{x1,x1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
({{}}) is non empty cap-closed subset-closed binary_complete () set
bool (union {{}}) is non empty cup-closed cap-closed diff-closed preBoolean finite V41() subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union {{}}) : for b<sub>2</sub> being Element of {{}} ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
union ({{}}) is set
C1 is set
(C1) is non empty cap-closed subset-closed binary_complete () set
id C1 is Relation-like C1 -defined C1 -valued V30(C1) V57() V59() V60() V64() Element of bool [:C1,C1:]
[:C1,C1:] is Relation-like set
bool [:C1,C1:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
CohSp (id C1) is non empty cap-closed subset-closed binary_complete () set
((C1)) is non empty cap-closed subset-closed binary_complete () set
union (C1) is set
bool (union (C1)) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union (C1)) : for b<sub>2</sub> being Element of (C1) ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
bool C1 is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
((bool C1)) is non empty cap-closed subset-closed binary_complete () set
union (bool C1) is set
bool (union (bool C1)) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (union (bool C1)) : for b<sub>2</sub> being Element of bool C1 ex b<sub>3</sub> being set st b<sub>1</sub> /\ b<sub>2</sub> c= {b<sub>3</sub>} } is set
C2 is set
C2 is set
x1 is Element of (C1)
C2 /\ x1 is set
0 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered Element of NAT
{0} is non empty trivial cap-closed finite V41() 1 -element subset-closed binary_complete () set
x1 is Element of (C1)
y1 is set
{y1} is non empty trivial finite 1 -element set
y1 is set
{y1} is non empty trivial finite 1 -element set
C2 /\ x1 is set
x2 is set
{x2} is non empty trivial finite 1 -element set
x1 is Element of (C1)
C1 is set
C2 is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
{2} is non empty trivial finite V41() 1 -element set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
[:C1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
len <*C1,C2*> is non empty V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal Element of NAT
dom <*C1,C2*> is non empty finite 2 -element Element of bool NAT
x1 is set
x1 `2 is set
x1 `1 is set
[(x1 `1),(x1 `2)] is V31() set
{(x1 `1),(x1 `2)} is non empty finite set
{(x1 `1)} is non empty trivial finite 1 -element set
{{(x1 `1),(x1 `2)},{(x1 `1)}} is non empty finite V41() set
<*C1,C2*> . (x1 `2) is set
C1 is set
(C1,{}) is set
<*C1,{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,{}*> is Relation-like Function-like set
Union (disjoin <*C1,{}*>) is set
[:C1,{1}:] is Relation-like set
({},C1) is set
<*{},C1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{},C1*> is Relation-like Function-like set
Union (disjoin <*{},C1*>) is set
[:C1,{2}:] is Relation-like set
[:{},{2}:] is Relation-like finite set
[:C1,{1}:] \/ [:{},{2}:] is Relation-like set
[:C1,{1}:] \/ {} is Relation-like set
[:{},{1}:] is Relation-like finite set
[:{},{1}:] \/ [:C1,{2}:] is Relation-like set
{} \/ [:C1,{2}:] is Relation-like set
x1 is set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
x1 `1 is set
x1 `2 is set
[(x1 `1),(x1 `2)] is V31() set
{(x1 `1),(x1 `2)} is non empty finite set
{(x1 `1)} is non empty trivial finite 1 -element set
{{(x1 `1),(x1 `2)},{(x1 `1)}} is non empty finite V41() set
[:C1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
x1 is set
[x1,1] is V31() set
{x1,1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,1},{x1}} is non empty finite V41() set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
[:C1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
x1 is set
[x1,2] is V31() set
{x1,2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,2},{x1}} is non empty finite V41() set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
[:C1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
x2 is set
[x2,1] is V31() set
{x2,1} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,1},{x2}} is non empty finite V41() set
x2 is set
[x2,2] is V31() set
{x2,2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,2},{x2}} is non empty finite V41() set
x2 is set
x2 `2 is set
x2 `1 is set
[(x2 `1),(x2 `2)] is V31() set
{(x2 `1),(x2 `2)} is non empty finite set
{(x2 `1)} is non empty trivial finite 1 -element set
{{(x2 `1),(x2 `2)},{(x2 `1)}} is non empty finite V41() set
x1 is set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
[:C1,{1}:] is Relation-like set
x1 /\ [:C1,{1}:] is Relation-like set
proj1 (x1 /\ [:C1,{1}:]) is set
y1 is set
[:C2,{2}:] is Relation-like set
x1 /\ [:C2,{2}:] is Relation-like set
proj1 (x1 /\ [:C2,{2}:]) is set
x2 is set
(y1,x2) is set
<*y1,x2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y1,x2*> is Relation-like Function-like set
Union (disjoin <*y1,x2*>) is set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
y2 is set
y2 `1 is set
y2 `2 is set
[(y2 `1),(y2 `2)] is V31() set
{(y2 `1),(y2 `2)} is non empty finite set
{(y2 `1)} is non empty trivial finite 1 -element set
{{(y2 `1),(y2 `2)},{(y2 `1)}} is non empty finite V41() set
y2 is set
y2 `1 is set
y2 `2 is set
[(y2 `1),(y2 `2)] is V31() set
{(y2 `1),(y2 `2)} is non empty finite set
{(y2 `1)} is non empty trivial finite 1 -element set
{{(y2 `1),(y2 `2)},{(y2 `1)}} is non empty finite V41() set
x is set
[(y2 `1),x] is V31() set
{(y2 `1),x} is non empty finite set
{{(y2 `1),x},{(y2 `1)}} is non empty finite V41() set
x is set
[(y2 `1),x] is V31() set
{(y2 `1),x} is non empty finite set
{{(y2 `1),x},{(y2 `1)}} is non empty finite V41() set
proj1 [:C2,{2}:] is set
proj1 [:C1,{1}:] is set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
(C1,C2) \/ (x1,y1) is set
C1 \/ x1 is set
C2 \/ y1 is set
((C1 \/ x1),(C2 \/ y1)) is set
<*(C1 \/ x1),(C2 \/ y1)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(C1 \/ x1),(C2 \/ y1)*> is Relation-like Function-like set
Union (disjoin <*(C1 \/ x1),(C2 \/ y1)*>) is set
[:C1,{1}:] is Relation-like set
[:x1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:y1,{2}:] is Relation-like set
[:(C1 \/ x1),{1}:] is Relation-like set
[:(C2 \/ y1),{2}:] is Relation-like set
[:C1,{1}:] \/ [:x1,{1}:] is Relation-like set
[:(C1 \/ x1),{1}:] \/ [:(C2 \/ y1),{2}:] is Relation-like set
[:C2,{2}:] \/ [:y1,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
[:x1,{1}:] \/ [:y1,{2}:] is Relation-like set
([:C1,{1}:] \/ [:C2,{2}:]) \/ [:x1,{1}:] is Relation-like set
(([:C1,{1}:] \/ [:C2,{2}:]) \/ [:x1,{1}:]) \/ [:y1,{2}:] is Relation-like set
[:(C1 \/ x1),{1}:] \/ [:C2,{2}:] is Relation-like set
([:(C1 \/ x1),{1}:] \/ [:C2,{2}:]) \/ [:y1,{2}:] is Relation-like set
C1 is set
C2 is set
(C1,C2) is set
<*C1,C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*C1,C2*> is Relation-like Function-like set
Union (disjoin <*C1,C2*>) is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
(C1,C2) /\ (x1,y1) is set
C1 /\ x1 is set
C2 /\ y1 is set
((C1 /\ x1),(C2 /\ y1)) is set
<*(C1 /\ x1),(C2 /\ y1)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(C1 /\ x1),(C2 /\ y1)*> is Relation-like Function-like set
Union (disjoin <*(C1 /\ x1),(C2 /\ y1)*>) is set
[:C1,{1}:] is Relation-like set
[:x1,{1}:] is Relation-like set
[:C2,{2}:] is Relation-like set
[:y1,{2}:] is Relation-like set
[:(C1 /\ x1),{1}:] is Relation-like set
[:(C2 /\ y1),{2}:] is Relation-like set
[:C1,{1}:] /\ [:x1,{1}:] is Relation-like set
[:C2,{2}:] /\ [:y1,{2}:] is Relation-like set
[:C2,{2}:] /\ [:x1,{1}:] is Relation-like set
[:C1,{1}:] /\ [:y1,{2}:] is Relation-like set
[:C1,{1}:] \/ [:C2,{2}:] is Relation-like set
[:x1,{1}:] \/ [:y1,{2}:] is Relation-like set
([:C1,{1}:] \/ [:C2,{2}:]) /\ [:x1,{1}:] is Relation-like set
([:C1,{1}:] \/ [:C2,{2}:]) /\ [:y1,{2}:] is Relation-like set
(([:C1,{1}:] \/ [:C2,{2}:]) /\ [:x1,{1}:]) \/ (([:C1,{1}:] \/ [:C2,{2}:]) /\ [:y1,{2}:]) is Relation-like set
[:(C1 /\ x1),{1}:] \/ ([:C2,{2}:] /\ [:x1,{1}:]) is Relation-like set
([:(C1 /\ x1),{1}:] \/ ([:C2,{2}:] /\ [:x1,{1}:])) \/ (([:C1,{1}:] \/ [:C2,{2}:]) /\ [:y1,{2}:]) is Relation-like set
([:C1,{1}:] /\ [:y1,{2}:]) \/ [:(C2 /\ y1),{2}:] is Relation-like set
[:(C1 /\ x1),{1}:] \/ (([:C1,{1}:] /\ [:y1,{2}:]) \/ [:(C2 /\ y1),{2}:]) is Relation-like set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
y1 is non empty cap-closed subset-closed binary_complete () set
x2 is non empty cap-closed subset-closed binary_complete () set
x1 is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
y2 is set
x is Element of y1
y is Element of x2
(x,y) is set
<*x,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x,y*> is Relation-like Function-like set
Union (disjoin <*x,y*>) is set
(y1,x2) is set
{ (b₁,b₂) where b₁ is Element of y1, b₂ is Element of x2 : verum } is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
x2 is Element of C1
y2 is Element of C2
(x2,y2) is set
<*x2,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,y2*> is Relation-like Function-like set
Union (disjoin <*x2,y2*>) is set
x is Element of C1
y is Element of C2
x2 is Element of C1
y2 is Element of C2
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union (C1,C2) is set
union C1 is set
union C2 is set
((union C1),(union C2)) is set
<*(union C1),(union C2)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union C1),(union C2)*> is Relation-like Function-like set
Union (disjoin <*(union C1),(union C2)*>) is set
x1 is set
y1 is set
x2 is Element of C1
y2 is Element of C2
(x2,y2) is set
<*x2,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,y2*> is Relation-like Function-like set
Union (disjoin <*x2,y2*>) is set
x1 is set
x1 `1 is set
x1 `2 is set
[(x1 `1),(x1 `2)] is V31() set
{(x1 `1),(x1 `2)} is non empty finite set
{(x1 `1)} is non empty trivial finite 1 -element set
{{(x1 `1),(x1 `2)},{(x1 `1)}} is non empty finite V41() set
the Element of C2 is Element of C2
x2 is set
y2 is Element of C1
(y2, the Element of C2) is set
<*y2, the Element of C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y2, the Element of C2*> is Relation-like Function-like set
Union (disjoin <*y2, the Element of C2*>) is set
the Element of C1 is Element of C1
x2 is set
y2 is Element of C2
( the Element of C1,y2) is set
<* the Element of C1,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <* the Element of C1,y2*> is Relation-like Function-like set
Union (disjoin <* the Element of C1,y2*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
x1 is set
y1 is set
(x1,y1) is set
<*x1,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x1,y1*> is Relation-like Function-like set
Union (disjoin <*x1,y1*>) is set
x2 is Element of C1
(x2,{}) is set
<*x2,{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,{}*> is Relation-like Function-like set
Union (disjoin <*x2,{}*>) is set
x2 is Element of C2
({},x2) is set
<*{},x2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{},x2*> is Relation-like Function-like set
Union (disjoin <*{},x2*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
x1 is set
y1 is Element of C1
(y1,{}) is set
<*y1,{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y1,{}*> is Relation-like Function-like set
Union (disjoin <*y1,{}*>) is set
x2 is Element of C2
({},x2) is set
<*{},x2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{},x2*> is Relation-like Function-like set
Union (disjoin <*{},x2*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
union (C1,C2) is set
union C1 is set
union C2 is set
((union C1),(union C2)) is set
<*(union C1),(union C2)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union C1),(union C2)*> is Relation-like Function-like set
Union (disjoin <*(union C1),(union C2)*>) is set
x1 is set
y1 is set
x2 is Element of C1
y2 is Element of C2
(x2,y2) is set
<*x2,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,y2*> is Relation-like Function-like set
Union (disjoin <*x2,y2*>) is set
x1 is set
x1 `1 is set
x1 `2 is set
[(x1 `1),(x1 `2)] is V31() set
{(x1 `1),(x1 `2)} is non empty finite set
{(x1 `1)} is non empty trivial finite 1 -element set
{{(x1 `1),(x1 `2)},{(x1 `1)}} is non empty finite V41() set
x2 is set
y2 is Element of C1
y1 is Element of C2
(y2,y1) is set
<*y2,y1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y2,y1*> is Relation-like Function-like set
Union (disjoin <*y2,y1*>) is set
x2 is set
y1 is Element of C1
y2 is Element of C2
(y1,y2) is set
<*y1,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y1,y2*> is Relation-like Function-like set
Union (disjoin <*y1,y2*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
the Element of C1 is Element of C1
the Element of C2 is Element of C2
( the Element of C1, the Element of C2) is set
<* the Element of C1, the Element of C2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <* the Element of C1, the Element of C2*> is Relation-like Function-like set
Union (disjoin <* the Element of C1, the Element of C2*>) is set
x2 is set
x is Element of C1
y is Element of C2
(x,y) is set
<*x,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x,y*> is Relation-like Function-like set
Union (disjoin <*x,y*>) is set
y2 is set
b is set
z2 is set
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
x2 is set
union x2 is set
{ b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } is set
x is set
b is Element of C2
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
y is set
z1 is Element of C2
z is Element of C1
(z,z1) is set
<*z,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,z1*> is Relation-like Function-like set
Union (disjoin <*z,z1*>) is set
z is Element of C1
(z,z1) is set
<*z,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,z1*> is Relation-like Function-like set
Union (disjoin <*z,z1*>) is set
(z2,b) \/ (z,z1) is set
z2 \/ z is set
b \/ z1 is set
((z2 \/ z),(b \/ z1)) is set
<*(z2 \/ z),(b \/ z1)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(z2 \/ z),(b \/ z1)*> is Relation-like Function-like set
Union (disjoin <*(z2 \/ z),(b \/ z1)*>) is set
x \/ y is set
union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } is set
{ b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } is set
union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } is set
((union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } )) is set
<*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } )*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } )*> is Relation-like Function-like set
Union (disjoin <*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in x2 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in x2 } )*>) is set
y is set
y `1 is set
y `2 is set
[(y `1),(y `2)] is V31() set
{(y `1),(y `2)} is non empty finite set
{(y `1)} is non empty trivial finite 1 -element set
{{(y `1),(y `2)},{(y `1)}} is non empty finite V41() set
b is set
z2 is Element of C1
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
b is set
z2 is Element of C2
z1 is Element of C1
(z1,z2) is set
<*z1,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z1,z2*> is Relation-like Function-like set
Union (disjoin <*z1,z2*>) is set
z1 is Element of C1
(z1,z2) is set
<*z1,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z1,z2*> is Relation-like Function-like set
Union (disjoin <*z1,z2*>) is set
y is set
b is set
b \/ b is set
z2 is Element of C1
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
y is set
z2 is Element of C1
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
b is set
z is Element of C1
y is Element of C2
(z,y) is set
<*z,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,y*> is Relation-like Function-like set
Union (disjoin <*z,y*>) is set
y is Element of C2
(z,y) is set
<*z,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,y*> is Relation-like Function-like set
Union (disjoin <*z,y*>) is set
(z2,z1) \/ (z,y) is set
z2 \/ z is set
z1 \/ y is set
((z2 \/ z),(z1 \/ y)) is set
<*(z2 \/ z),(z1 \/ y)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(z2 \/ z),(z1 \/ y)*> is Relation-like Function-like set
Union (disjoin <*(z2 \/ z),(z1 \/ y)*>) is set
y \/ b is set
(C1,C2) is set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
the Element of C1 is Element of C1
( the Element of C1,{}) is set
<* the Element of C1,{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <* the Element of C1,{}*> is Relation-like Function-like set
Union (disjoin <* the Element of C1,{}*>) is set
y1 is set
y2 is Element of C1
x is Element of C2
(y2,x) is set
<*y2,x*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y2,x*> is Relation-like Function-like set
Union (disjoin <*y2,x*>) is set
x2 is set
y is set
b is set
(y,b) is set
<*y,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y,b*> is Relation-like Function-like set
Union (disjoin <*y,b*>) is set
y1 is set
union y1 is set
{ b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } is set
{ b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } is set
x is set
b is Element of C2
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
y is set
z1 is Element of C2
z is Element of C1
(z,z1) is set
<*z,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,z1*> is Relation-like Function-like set
Union (disjoin <*z,z1*>) is set
z is Element of C1
(z,z1) is set
<*z,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z,z1*> is Relation-like Function-like set
Union (disjoin <*z,z1*>) is set
(z2,b) \/ (z,z1) is set
z2 \/ z is set
b \/ z1 is set
((z2 \/ z),(b \/ z1)) is set
<*(z2 \/ z),(b \/ z1)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(z2 \/ z),(b \/ z1)*> is Relation-like Function-like set
Union (disjoin <*(z2 \/ z),(b \/ z1)*>) is set
x \/ y is set
union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } is set
union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } is set
((union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } )) is set
<*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } )*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } )*> is Relation-like Function-like set
Union (disjoin <*(union { b₁ where b₁ is Element of C1 : ex b₂ being Element of C2 st (b₁,b₂) in y1 } ),(union { b₁ where b₁ is Element of C2 : ex b₂ being Element of C1 st (b₂,b₁) in y1 } )*>) is set
x is set
x `1 is set
x `2 is set
[(x `1),(x `2)] is V31() set
{(x `1),(x `2)} is non empty finite set
{(x `1)} is non empty trivial finite 1 -element set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V41() set
y is set
b is Element of C1
z2 is Element of C2
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
z2 is Element of C2
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
y is set
b is Element of C2
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
z2 is Element of C1
(z2,b) is set
<*z2,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,b*> is Relation-like Function-like set
Union (disjoin <*z2,b*>) is set
x is set
y is set
y \/ y is set
b is Element of C1
z2 is Element of C2
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
x is non empty set
the Element of x is Element of x
b is set
z2 is Element of C1
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
z1 is Element of C2
(z2,z1) is set
<*z2,z1*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z2,z1*> is Relation-like Function-like set
Union (disjoin <*z2,z1*>) is set
z is non empty set
the Element of z is Element of z
zz is set
y is Element of C2
ay is Element of C1
(ay,y) is set
<*ay,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*ay,y*> is Relation-like Function-like set
Union (disjoin <*ay,y*>) is set
ay is Element of C1
(ay,y) is set
<*ay,y*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*ay,y*> is Relation-like Function-like set
Union (disjoin <*ay,y*>) is set
(z2,z1) \/ (ay,y) is set
z2 \/ ay is set
z1 \/ y is set
((z2 \/ ay),(z1 \/ y)) is set
<*(z2 \/ ay),(z1 \/ y)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(z2 \/ ay),(z1 \/ y)*> is Relation-like Function-like set
Union (disjoin <*(z2 \/ ay),(z1 \/ y)*>) is set
x is set
b is Element of C1
z2 is Element of C2
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
z2 is Element of C2
(b,z2) is set
<*b,z2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*b,z2*> is Relation-like Function-like set
Union (disjoin <*b,z2*>) is set
y is set
z1 is Element of C1
z is Element of C2
(z1,z) is set
<*z1,z*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z1,z*> is Relation-like Function-like set
Union (disjoin <*z1,z*>) is set
z is Element of C2
(z1,z) is set
<*z1,z*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*z1,z*> is Relation-like Function-like set
Union (disjoin <*z1,z*>) is set
(b,z2) \/ (z1,z) is set
b \/ z1 is set
z2 \/ z is set
((b \/ z1),(z2 \/ z)) is set
<*(b \/ z1),(z2 \/ z)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(b \/ z1),(z2 \/ z)*> is Relation-like Function-like set
Union (disjoin <*(b \/ z1),(z2 \/ z)*>) is set
x \/ y is set
C1 is non empty cap-closed subset-closed binary_complete () set
Web C1 is Relation-like union C1 -defined union C1 -valued V30( union C1) V57() V59() Element of bool [:(union C1),(union C1):]
union C1 is set
[:(union C1),(union C1):] is Relation-like set
bool [:(union C1),(union C1):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
[x1,1] is V31() set
{x1,1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,1},{x1}} is non empty finite V41() set
y1 is set
[y1,1] is V31() set
{y1,1} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,1},{y1}} is non empty finite V41() set
[[x1,1],[y1,1]] is V31() set
{[x1,1],[y1,1]} is non empty Relation-like finite set
{[x1,1]} is non empty trivial Relation-like finite 1 -element set
{{[x1,1],[y1,1]},{[x1,1]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
[:{x1,y1},{1}:] is non empty Relation-like finite set
({x1,y1},{}) is set
<*{x1,y1},{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{x1,y1},{}*> is Relation-like Function-like set
Union (disjoin <*{x1,y1},{}*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
Web C2 is Relation-like union C2 -defined union C2 -valued V30( union C2) V57() V59() Element of bool [:(union C2),(union C2):]
union C2 is set
[:(union C2),(union C2):] is Relation-like set
bool [:(union C2),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
[x1,2] is V31() set
{x1,2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,2},{x1}} is non empty finite V41() set
y1 is set
[y1,2] is V31() set
{y1,2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,2},{y1}} is non empty finite V41() set
[[x1,2],[y1,2]] is V31() set
{[x1,2],[y1,2]} is non empty Relation-like finite set
{[x1,2]} is non empty trivial Relation-like finite 1 -element set
{{[x1,2],[y1,2]},{[x1,2]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
[:{x1,y1},{2}:] is non empty Relation-like finite set
({},{x1,y1}) is set
<*{},{x1,y1}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{},{x1,y1}*> is Relation-like Function-like set
Union (disjoin <*{},{x1,y1}*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
union C1 is set
C2 is non empty cap-closed subset-closed binary_complete () set
union C2 is set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
y1 is set
[x1,1] is V31() set
{x1,1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,1},{x1}} is non empty finite V41() set
[y1,2] is V31() set
{y1,2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,2},{y1}} is non empty finite V41() set
[[x1,1],[y1,2]] is V31() set
{[x1,1],[y1,2]} is non empty Relation-like finite set
{[x1,1]} is non empty trivial Relation-like finite 1 -element set
{{[x1,1],[y1,2]},{[x1,1]}} is non empty finite V41() set
[[y1,2],[x1,1]] is V31() set
{[y1,2],[x1,1]} is non empty Relation-like finite set
{[y1,2]} is non empty trivial Relation-like finite 1 -element set
{{[y1,2],[x1,1]},{[y1,2]}} is non empty finite V41() set
({x1},{y1}) is set
<*{x1},{y1}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{x1},{y1}*> is Relation-like Function-like set
Union (disjoin <*{x1},{y1}*>) is set
[:{x1},{1}:] is non empty Relation-like finite set
[:{y1},{2}:] is non empty Relation-like finite set
[:{x1},{1}:] \/ [:{y1},{2}:] is non empty Relation-like finite set
{[x1,1]} \/ [:{y1},{2}:] is non empty Relation-like finite set
{[x1,1]} \/ {[y1,2]} is non empty Relation-like finite set
C1 is non empty cap-closed subset-closed binary_complete () set
Web C1 is Relation-like union C1 -defined union C1 -valued V30( union C1) V57() V59() Element of bool [:(union C1),(union C1):]
union C1 is set
[:(union C1),(union C1):] is Relation-like set
bool [:(union C1),(union C1):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
[x1,1] is V31() set
{x1,1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,1},{x1}} is non empty finite V41() set
y1 is set
[y1,1] is V31() set
{y1,1} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,1},{y1}} is non empty finite V41() set
[[x1,1],[y1,1]] is V31() set
{[x1,1],[y1,1]} is non empty Relation-like finite set
{[x1,1]} is non empty trivial Relation-like finite 1 -element set
{{[x1,1],[y1,1]},{[x1,1]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
({x1,y1},{}) is set
<*{x1,y1},{}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{x1,y1},{}*> is Relation-like Function-like set
Union (disjoin <*{x1,y1},{}*>) is set
[:{x1,y1},{1}:] is non empty Relation-like finite set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
Web C2 is Relation-like union C2 -defined union C2 -valued V30( union C2) V57() V59() Element of bool [:(union C2),(union C2):]
union C2 is set
[:(union C2),(union C2):] is Relation-like set
bool [:(union C2),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
[x1,2] is V31() set
{x1,2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,2},{x1}} is non empty finite V41() set
y1 is set
[y1,2] is V31() set
{y1,2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,2},{y1}} is non empty finite V41() set
[[x1,2],[y1,2]] is V31() set
{[x1,2],[y1,2]} is non empty Relation-like finite set
{[x1,2]} is non empty trivial Relation-like finite 1 -element set
{{[x1,2],[y1,2]},{[x1,2]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
({},{x1,y1}) is set
<*{},{x1,y1}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{},{x1,y1}*> is Relation-like Function-like set
Union (disjoin <*{},{x1,y1}*>) is set
[:{x1,y1},{2}:] is non empty Relation-like finite set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,{}) where b₁ is Element of C1 : verum } is set
{ ({},b₁) where b₁ is Element of C2 : verum } is set
{ (b₁,{}) where b₁ is Element of C1 : verum } \/ { ({},b₁) where b₁ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
[x1,1] is V31() set
{x1,1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,1},{x1}} is non empty finite V41() set
y1 is set
[y1,2] is V31() set
{y1,2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,2},{y1}} is non empty finite V41() set
[[x1,1],[y1,2]] is V31() set
{[x1,1],[y1,2]} is non empty Relation-like finite set
{[x1,1]} is non empty trivial Relation-like finite 1 -element set
{{[x1,1],[y1,2]},{[x1,1]}} is non empty finite V41() set
[[y1,2],[x1,1]] is V31() set
{[y1,2],[x1,1]} is non empty Relation-like finite set
{[y1,2]} is non empty trivial Relation-like finite 1 -element set
{{[y1,2],[x1,1]},{[y1,2]}} is non empty finite V41() set
({x1},{y1}) is set
<*{x1},{y1}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{x1},{y1}*> is Relation-like Function-like set
Union (disjoin <*{x1},{y1}*>) is set
[:{x1},{1}:] is non empty Relation-like finite set
[:{y1},{2}:] is non empty Relation-like finite set
[:{x1},{1}:] \/ [:{y1},{2}:] is non empty Relation-like finite set
{[x1,1]} \/ [:{y1},{2}:] is non empty Relation-like finite set
{[x1,1]} \/ {[y1,2]} is non empty Relation-like finite set
C1 is non empty cap-closed subset-closed binary_complete () set
(C1) is non empty cap-closed subset-closed binary_complete () set
union C1 is set
bool (union C1) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b₁ where b₁ is Element of bool (union C1) : for b₂ being Element of C1 ex b₃ being set st b₁ /\ b₂ c= {b₃} } is set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,b₂) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
((C1,C2)) is non empty cap-closed subset-closed binary_complete () set
union (C1,C2) is set
bool (union (C1,C2)) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b₁ where b₁ is Element of bool (union (C1,C2)) : for b₂ being Element of (C1,C2) ex b₃ being set st b₁ /\ b₂ c= {b₃} } is set
(C2) is non empty cap-closed subset-closed binary_complete () set
union C2 is set
bool (union C2) is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
{ b₁ where b₁ is Element of bool (union C2) : for b₂ being Element of C2 ex b₃ being set st b₁ /\ b₂ c= {b₃} } is set
((C1),(C2)) is non empty cap-closed subset-closed binary_complete () set
{ (b₁,{}) where b₁ is Element of (C1) : verum } is set
{ ({},b₁) where b₁ is Element of (C2) : verum } is set
{ (b₁,{}) where b₁ is Element of (C1) : verum } \/ { ({},b₁) where b₁ is Element of (C2) : verum } is set
y1 is set
((union C1),(union C2)) is set
<*(union C1),(union C2)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union C1),(union C2)*> is Relation-like Function-like set
Union (disjoin <*(union C1),(union C2)*>) is set
x2 is set
y2 is set
(x2,y2) is set
<*x2,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,y2*> is Relation-like Function-like set
Union (disjoin <*x2,y2*>) is set
y is Element of C1
x is Element of C2
(y,x) is set
<*y,x*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y,x*> is Relation-like Function-like set
Union (disjoin <*y,x*>) is set
y1 /\ (y,x) is set
b is set
{b} is non empty trivial finite 1 -element set
x2 /\ y is set
y2 /\ x is set
((x2 /\ y),(y2 /\ x)) is set
<*(x2 /\ y),(y2 /\ x)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(x2 /\ y),(y2 /\ x)*> is Relation-like Function-like set
Union (disjoin <*(x2 /\ y),(y2 /\ x)*>) is set
[:(x2 /\ y),{1}:] is Relation-like set
[:(y2 /\ x),{2}:] is Relation-like set
[:(x2 /\ y),{1}:] \/ [:(y2 /\ x),{2}:] is Relation-like set
0 is empty V8() V9() V10() V12() V13() V14() V15() V16() V17() V19() Relation-like non-empty empty-yielding functional finite finite-yielding V41() cardinal {} -element FinSequence-like FinSequence-membered Element of NAT
{0} is non empty trivial cap-closed finite V41() 1 -element subset-closed binary_complete () set
z2 is non empty set
the Element of z2 is Element of z2
z is set
y is set
{y} is non empty trivial finite 1 -element set
zz is set
[zz,1] is V31() set
{zz,1} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,1},{zz}} is non empty finite V41() set
[ the Element of z2,1] is V31() set
{ the Element of z2,1} is non empty finite set
{ the Element of z2} is non empty trivial finite 1 -element set
{{ the Element of z2,1},{ the Element of z2}} is non empty finite V41() set
z2 is set
{z2} is non empty trivial finite 1 -element set
y is Element of C1
b is Element of C2
(y,b) is set
<*y,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y,b*> is Relation-like Function-like set
Union (disjoin <*y,b*>) is set
y1 /\ (y,b) is set
z2 is set
{z2} is non empty trivial finite 1 -element set
x is Element of (C1)
x /\ y is set
y2 /\ b is set
((x /\ y),(y2 /\ b)) is set
<*(x /\ y),(y2 /\ b)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(x /\ y),(y2 /\ b)*> is Relation-like Function-like set
Union (disjoin <*(x /\ y),(y2 /\ b)*>) is set
[:(y2 /\ b),{2}:] is Relation-like set
[:(x /\ y),{1}:] is Relation-like set
[:(x /\ y),{1}:] \/ [:(y2 /\ b),{2}:] is Relation-like set
z1 is non empty set
the Element of z1 is Element of z1
y is set
zz is set
{zz} is non empty trivial finite 1 -element set
y is set
[y,2] is V31() set
{y,2} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,2},{y}} is non empty finite V41() set
[ the Element of z1,2] is V31() set
{ the Element of z1,2} is non empty finite set
{ the Element of z1} is non empty trivial finite 1 -element set
{{ the Element of z1,2},{ the Element of z1}} is non empty finite V41() set
z1 is set
{z1} is non empty trivial finite 1 -element set
y is Element of (C2)
b is non empty set
the Element of b is Element of b
z2 is non empty set
the Element of z2 is Element of z2
union (C2) is set
{ the Element of z2} is non empty trivial finite 1 -element set
union (C1) is set
{ the Element of b} is non empty trivial finite 1 -element set
({ the Element of b},{ the Element of z2}) is set
<*{ the Element of b},{ the Element of z2}*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*{ the Element of b},{ the Element of z2}*> is Relation-like Function-like set
Union (disjoin <*{ the Element of b},{ the Element of z2}*>) is set
y1 /\ ({ the Element of b},{ the Element of z2}) is set
y is set
{y} is non empty trivial finite 1 -element set
b /\ { the Element of b} is finite set
z2 /\ { the Element of z2} is finite set
((b /\ { the Element of b}),(z2 /\ { the Element of z2})) is set
<*(b /\ { the Element of b}),(z2 /\ { the Element of z2})*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(b /\ { the Element of b}),(z2 /\ { the Element of z2})*> is Relation-like Function-like set
Union (disjoin <*(b /\ { the Element of b}),(z2 /\ { the Element of z2})*>) is set
[ the Element of z2,2] is V31() set
{ the Element of z2,2} is non empty finite set
{{ the Element of z2,2},{ the Element of z2}} is non empty finite V41() set
[ the Element of b,1] is V31() set
{ the Element of b,1} is non empty finite set
{{ the Element of b,1},{ the Element of b}} is non empty finite V41() set
y1 is set
x2 is Element of (C1)
y2 is Element of (C2)
(x2,y2) is set
<*x2,y2*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*x2,y2*> is Relation-like Function-like set
Union (disjoin <*x2,y2*>) is set
x is Element of (C1,C2)
y1 /\ x is set
y is Element of C1
b is Element of C2
(y,b) is set
<*y,b*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*y,b*> is Relation-like Function-like set
Union (disjoin <*y,b*>) is set
x2 /\ y is set
y2 /\ b is set
((x2 /\ y),(y2 /\ b)) is set
<*(x2 /\ y),(y2 /\ b)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(x2 /\ y),(y2 /\ b)*> is Relation-like Function-like set
Union (disjoin <*(x2 /\ y),(y2 /\ b)*>) is set
z2 is set
{z2} is non empty trivial finite 1 -element set
z1 is set
{z1} is non empty trivial finite 1 -element set
[z2,2] is V31() set
{z2,2} is non empty finite set
{{z2,2},{z2}} is non empty finite V41() set
[z1,1] is V31() set
{z1,1} is non empty finite set
{{z1,1},{z1}} is non empty finite V41() set
z is set
{z} is non empty trivial finite 1 -element set
y is set
y `1 is set
y `2 is set
[(y `1),(y `2)] is V31() set
{(y `1),(y `2)} is non empty finite set
{(y `1)} is non empty trivial finite 1 -element set
{{(y `1),(y `2)},{(y `1)}} is non empty finite V41() set
union (C2) is set
union (C1) is set
((union C1),(union C2)) is set
<*(union C1),(union C2)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
disjoin <*(union C1),(union C2)*> is Relation-like Function-like set
Union (disjoin <*(union C1),(union C2)*>) is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
x1 is set
y1 is set
x2 is Element of C1
y2 is Element of C2
[:x2,y2:] is Relation-like set
bool [:x2,y2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x is Element of C1
y is Element of C2
[:x,y:] is Relation-like set
y1 is Element of C1
x2 is Element of C2
[:y1,x2:] is Relation-like set
bool [:y1,x2:] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
the Element of C1 is Element of C1
the Element of C2 is Element of C2
[: the Element of C1, the Element of C2:] is Relation-like set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
x1 is Element of (C1,C2)
proj1 x1 is set
proj2 x1 is set
[:(proj1 x1),(proj2 x1):] is Relation-like set
y1 is Element of C1
x2 is Element of C2
[:y1,x2:] is Relation-like set
y2 is set
y2 `1 is set
y2 `2 is set
[(y2 `1),(y2 `2)] is V31() set
{(y2 `1),(y2 `2)} is non empty finite set
{(y2 `1)} is non empty trivial finite 1 -element set
{{(y2 `1),(y2 `2)},{(y2 `1)}} is non empty finite V41() set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
x1 is set
y1 is set
x2 is Element of C1
y2 is Element of C2
[:x2,y2:] is Relation-like set
x1 is set
union x1 is set
{ (proj1 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } is set
{ (proj2 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } is set
y2 is set
y is Element of (C1,C2)
proj2 y is set
x is set
b is Element of (C1,C2)
proj2 b is set
y \/ b is set
proj2 (y \/ b) is set
y2 \/ x is set
union { (proj2 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } is set
union { (proj1 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } is set
[:(union { (proj1 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } ),(union { (proj2 b₁) where b₁ is Element of (C1,C2) : b₁ in x1 } ):] is Relation-like set
y2 is set
x is set
x \/ x is set
proj2 x is set
proj1 x is set
[:(proj1 x),(proj2 x):] is Relation-like set
y2 is set
y is Element of (C1,C2)
proj1 y is set
x is set
b is Element of (C1,C2)
proj1 b is set
y \/ b is set
proj1 (y \/ b) is set
y2 \/ x is set
C1 is non empty cap-closed subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union (C1,C2) is set
union C1 is set
union C2 is set
[:(union C1),(union C2):] is Relation-like set
x1 is set
y1 is set
x2 is Element of C1
y2 is Element of C2
[:x2,y2:] is Relation-like set
x1 is set
y1 is set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,y1},{x1}} is non empty finite V41() set
x2 is set
y2 is set
[:x2,y2:] is Relation-like set
C1 is non empty cap-closed subset-closed binary_complete () set
Web C1 is Relation-like union C1 -defined union C1 -valued V30( union C1) V57() V59() Element of bool [:(union C1),(union C1):]
union C1 is set
[:(union C1),(union C1):] is Relation-like set
bool [:(union C1),(union C1):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
C2 is non empty cap-closed subset-closed binary_complete () set
(C1,C2) is non empty cap-closed subset-closed binary_complete () set
{ (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
union { (bool [:b₁,b₂:]) where b₁ is Element of C1, b₂ is Element of C2 : verum } is set
Web (C1,C2) is Relation-like union (C1,C2) -defined union (C1,C2) -valued V30( union (C1,C2)) V57() V59() Element of bool [:(union (C1,C2)),(union (C1,C2)):]
union (C1,C2) is set
[:(union (C1,C2)),(union (C1,C2)):] is Relation-like set
bool [:(union (C1,C2)),(union (C1,C2)):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
Web C2 is Relation-like union C2 -defined union C2 -valued V30( union C2) V57() V59() Element of bool [:(union C2),(union C2):]
union C2 is set
[:(union C2),(union C2):] is Relation-like set
bool [:(union C2),(union C2):] is non empty cup-closed cap-closed diff-closed preBoolean subset-closed binary_complete () set
x1 is set
x2 is set
[x1,x2] is V31() set
{x1,x2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,x2},{x1}} is non empty finite V41() set
y1 is set
y2 is set
[y1,y2] is V31() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V41() set
[[x1,x2],[y1,y2]] is V31() set
{[x1,x2],[y1,y2]} is non empty Relation-like finite set
{[x1,x2]} is non empty trivial Relation-like finite 1 -element set
{{[x1,x2],[y1,y2]},{[x1,x2]}} is non empty finite V41() set
[x1,y1] is V31() set
{x1,y1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V41() set
[x2,y2] is V31() set
{x2,y2} is non empty finite set
{x2} is non empty trivial finite 1 -element set
{{x2,y2},{x2}} is non empty finite V41() set
[:{x1,y1},{x2,y2}:] is non empty Relation-like finite set
x is set
y is set
[x,y] is V31() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
proj1 {[x1,x2],[y1,y2]} is non empty finite set
proj2 {[x1,x2],[y1,y2]} is non empty finite set