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

F

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

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

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

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