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

NAT is non empty non trivial V8() V9() V10() non finite cardinal limit_cardinal set

K262() is L6()
the U1 of K262() is 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

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

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 Element of bool C1

C2 is set

x1 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

CohSp (id C1) is non empty subset-closed binary_complete set
C1 is non empty subset-closed set
(C1) is Element of bool C1

the Element of C1 is Element of C1
x1 is set
y1 is set

F1() is set
F2() is set
C2 is set
C1 is finite 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

union ({} C1) is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal set
C2 is set
C1 is set

C2 is set
C1 is 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

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

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

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

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

the Element of C1 is Element of C1
{ the Element of C1} is non empty trivial finite 1 -element set
C1 is 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

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

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

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

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

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

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

C2 is Element of bool C1
union C2 is set

C1 is non empty () 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

proj1 C1 is 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)

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

proj1 C1 is 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

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 set
proj1 C1 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

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

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

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 () 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

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

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

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

(x1,(x1,y1)) is Element of x1
C1 . (x1,(x1,y1)) is set

proj1 C1 is set
x1 is set
y1 is set
C1 . x1 is set

{ b1 where b1 is Element of bool x1 : b1 is finite } is set
x2 is 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

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

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

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

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

{ b1 where b1 is Element of bool x : x2 in C1 . b1 } 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

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

proj1 C1 is set

x1 is set
y1 is set
C1 . x1 is set
x2 is set
C1 . x2 is set

C1 . {} is set

union (C1 .: {}) is V8() V9() V10() V14() V15() V16() V17() V19() finite cardinal set
y2 is non empty set
{ {b1} where b1 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 . () 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

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

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

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

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

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

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

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

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

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

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

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

[:C1,C2:] is non empty Relation-like set

x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]

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

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

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

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

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

[:C1,C2:] is non empty Relation-like 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

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

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

(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

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

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

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

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

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

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

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

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

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

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

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

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

[:C1,C2:] is non empty Relation-like set

x1 is Relation-like C1 -defined union C2 -valued Element of bool [:C1,(union C2):]

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

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

[:C1,C2:] is non empty Relation-like 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

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

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

(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

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

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

union C2 is set
[:C1,(union C2):] is Relation-like 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

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

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

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

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