consider a' being Element of C1;
a' U+ {} in C1 "\/" C2 by Th87;
hence not C1 "\/" C2 is empty ; :: thesis: ( C1 "\/" C2 is subset-closed & C1 "\/" C2 is binary_complete )

hereby :: according to CLASSES1:def 1 :: thesis: C1 "\/" C2 is binary_complete

let a, b be set ; :: thesis: ( a in C1 "\/" C2 & b c= a implies b in C1 "\/" C2 )
assume a in C1 "\/" C2 ; :: thesis: ( b c= a implies b in C1 "\/" C2 )
then consider aa being Element of C1, bb being Element of C2 such that
A26: ( a = aa U+ bb & ( aa = {} or bb = {} ) ) by Th88;
assume b c= a ; :: thesis: b in C1 "\/" C2
then consider x1, y1 being set such that
A27: ( b = x1 U+ y1 & x1 c= aa & y1 c= bb ) by A26, Th80;
( x1 in C1 & y1 in C2 & ( x1 = {} or y1 = {} ) ) by A26, A27, CLASSES1:def 1;
hence b in C1 "\/" C2 by A27, Th87; :: thesis: verum

end;

let A be set ; :: according to COHSP_1:def 1 :: thesis: ( ( for a, b being set st a in A & b in A holds
a \/ b in C1 "\/" C2 ) implies union A in C1 "\/" C2 )
assume A28: for a, b being set st a in A & b in A holds
a \/ b in C1 "\/" C2 ; :: thesis: union A in C1 "\/" C2
set A1 = { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ;
set A2 = { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ;

now

let x, y be set ; :: thesis: ( x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } & y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } implies x \/ y in C1 )
assume x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ; :: thesis: ( y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } implies x \/ y in C1 )
then consider ax being Element of C1 such that
A29: ( x = ax & ex b being Element of C2 st ax U+ b in A ) ;
consider bx being Element of C2 such that
A30: ax U+ bx in A by A29;
assume y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ; :: thesis: x \/ y in C1
then consider ay being Element of C1 such that
A31: ( y = ay & ex b being Element of C2 st ay U+ b in A ) ;
consider by1 being Element of C2 such that
A32: ay U+ by1 in A by A31;
(ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A28, A30, A32;
then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th82;
then ( x \/ y in C1 or x \/ y = {} ) by A29, A31, Th87;
hence x \/ y in C1 by COH_SP:1; :: thesis: verum

end;

then A33: union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } in C1 by Def1;

now

let x, y be set ; :: thesis: ( x in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } & y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } implies x \/ y in C2 )
assume x in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ; :: thesis: ( y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } implies x \/ y in C2 )
then consider ax being Element of C2 such that
A34: ( x = ax & ex b being Element of C1 st b U+ ax in A ) ;
consider bx being Element of C1 such that
A35: bx U+ ax in A by A34;
assume y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ; :: thesis: x \/ y in C2
then consider ay being Element of C2 such that
A36: ( y = ay & ex b being Element of C1 st b U+ ay in A ) ;
consider by1 being Element of C1 such that
A37: by1 U+ ay in A by A36;
(bx U+ ax) \/ (by1 U+ ay) in C1 "\/" C2 by A28, A35, A37;
then (bx \/ by1) U+ (ax \/ ay) in C1 "\/" C2 by Th82;
then ( x \/ y in C2 or x \/ y = {} ) by A34, A36, Th87;
hence x \/ y in C2 by COH_SP:1; :: thesis: verum

end;

then A38: union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } in C2 by Def1;

A39: now

assume union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } <> {} ; :: thesis: not union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } <> {}
then reconsider AA = union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } as non empty set ;
consider aa being Element of AA;
consider x being set such that
A40: ( aa in x & x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) by TARSKI:def 4;
consider ax being Element of C1 such that
A41: ( x = ax & ex b being Element of C2 st ax U+ b in A ) by A40;
consider bx being Element of C2 such that
A42: ax U+ bx in A by A41;
assume union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } <> {} ; :: thesis: contradiction
then reconsider AA = union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } as non empty set ;
consider bb being Element of AA;
consider y being set such that
A43: ( bb in y & y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by TARSKI:def 4;
consider by1 being Element of C2 such that
A44: ( y = by1 & ex a being Element of C1 st a U+ by1 in A ) by A43;
consider ay being Element of C1 such that
A45: ay U+ by1 in A by A44;
(ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A28, A42, A45;
then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th82;
then ( ( x \/ ay = {} & aa in x \/ ay ) or ( bx \/ y = {} & bb in bx \/ y ) ) by A40, A41, A43, A44, Th87;
hence contradiction ; :: thesis: verum

end;

(union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) = union A

proof

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: union A c= (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } )

let x be set ; :: thesis: ( x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) implies b₁ in union A )
assume A46: x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ; :: thesis: b₁ in union A
then A47: ( x = [(x `1 ),(x `2 )] & ( ( x `2 = 1 & x `1 in union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) or ( x `2 = 2 & x `1 in union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ) ) by Th76;

per cases ( ( x `2 = 1 & x `1 in union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) or ( x `2 = 2 & x `1 in union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ) by A46, Th76;

suppose A48: ( x `2 = 1 & x `1 in union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) ; :: thesis: b₁ in union A

then consider a being set such that
A49: ( x `1 in a & a in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) by TARSKI:def 4;
consider ax being Element of C1 such that
A50: ( a = ax & ex b being Element of C2 st ax U+ b in A ) by A49;
consider bx being Element of C2 such that
A51: ax U+ bx in A by A50;
x in ax U+ bx by A47, A48, A49, A50, Th77;
hence x in union A by A51, TARSKI:def 4; :: thesis: verum

end;

suppose A52: ( x `2 = 2 & x `1 in union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ; :: thesis: b₁ in union A

then consider a being set such that
A53: ( x `1 in a & a in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by TARSKI:def 4;
consider bx being Element of C2 such that
A54: ( a = bx & ex a being Element of C1 st a U+ bx in A ) by A53;
consider ax being Element of C1 such that
A55: ax U+ bx in A by A54;
x in ax U+ bx by A47, A52, A53, A54, Th78;
hence x in union A by A55, TARSKI:def 4; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) )
assume x in union A ; :: thesis: x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } )
then consider a being set such that
A56: ( x in a & a in A ) by TARSKI:def 4;
a \/ a in C1 "\/" C2 by A28, A56;
then consider aa being Element of C1, bb being Element of C2 such that
A57: ( a = aa U+ bb & ( aa = {} or bb = {} ) ) by Th88;
( aa in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } & bb in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by A56, A57;
then ( aa c= union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } & bb c= union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by ZFMISC_1:92;
then aa U+ bb c= (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by Th79;
hence x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by A56, A57; :: thesis: verum

end;

hence union A in C1 "\/" C2 by A33, A38, A39, Th87; :: thesis: verum