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