consider a' being Element of C1, b' being Element of C2;
a' U+ b' in C1 "/\" C2 ;
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
A1: a = aa U+ bb ;
assume b c= a ; :: thesis: b in C1 "/\" C2
then consider x1, y1 being set such that
A2: ( b = x1 U+ y1 & x1 c= aa & y1 c= bb ) by A1, Th80;
( x1 in C1 & y1 in C2 ) by A2, CLASSES1:def 1;
hence b in C1 "/\" C2 by A2; :: 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 A3: 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
A4: ( x = ax & ex b being Element of C2 st ax U+ b in A ) ;
consider bx being Element of C2 such that
A5: ax U+ bx in A by A4;
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
A6: ( y = ay & ex b being Element of C2 st ay U+ b in A ) ;
consider by1 being Element of C2 such that
A7: ay U+ by1 in A by A6;
(ax U+ bx) \/ (ay U+ by1) in C1 "/\" C2 by A3, A5, A7;
then (ax \/ ay) U+ (bx \/ by1) in C1 "/\" C2 by Th82;
hence x \/ y in C1 by A4, A6, Th85; :: thesis: verum

end;

then A8: 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
A9: ( x = ax & ex b being Element of C1 st b U+ ax in A ) ;
consider bx being Element of C1 such that
A10: bx U+ ax in A by A9;
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
A11: ( y = ay & ex b being Element of C1 st b U+ ay in A ) ;
consider by1 being Element of C1 such that
A12: by1 U+ ay in A by A11;
(bx U+ ax) \/ (by1 U+ ay) in C1 "/\" C2 by A3, A10, A12;
then (bx \/ by1) U+ (ax \/ ay) in C1 "/\" C2 by Th82;
hence x \/ y in C2 by A9, A11, Th85; :: thesis: verum

end;

then A13: union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } in C2 by Def1;
(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 A14: 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 A15: ( 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 A14, Th76;

suppose A16: ( 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
A17: ( 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
A18: ( a = ax & ex b being Element of C2 st ax U+ b in A ) by A17;
consider bx being Element of C2 such that
A19: ax U+ bx in A by A18;
x in ax U+ bx by A15, A16, A17, A18, Th77;
hence x in union A by A19, TARSKI:def 4; :: thesis: verum

end;

suppose A20: ( 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
A21: ( 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
A22: ( a = bx & ex a being Element of C1 st a U+ bx in A ) by A21;
consider ax being Element of C1 such that
A23: ax U+ bx in A by A22;
x in ax U+ bx by A15, A20, A21, A22, Th78;
hence x in union A by A23, 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
A24: ( x in a & a in A ) by TARSKI:def 4;
a \/ a in C1 "/\" C2 by A3, A24;
then consider aa being Element of C1, bb being Element of C2 such that
A25: a = aa U+ bb ;
( 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 A24, A25;
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 A24, A25; :: thesis: verum

end;

hence union A in C1 "/\" C2 by A8, A13; :: thesis: verum