thus C1 [*] C2 is subset-closed :: thesis: C1 [*] C2 is binary_complete

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in C1 [*] C2 or not b c= a or b in C1 [*] C2 )
assume a in C1 [*] C2 ; :: thesis: ( not b c= a or b in C1 [*] C2 )
then consider a1 being Element of C1, a2 being Element of C2 such that
A1: a c= [:a1,a2:] by Th97;
assume b c= a ; :: thesis: b in C1 [*] C2
then b c= [:a1,a2:] by A1, XBOOLE_1:1;
hence b in C1 [*] C2 by Th97; :: 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 A2: 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 = { (proj1 a) where a is Element of C1 [*] C2 : a in A } ;
set A2 = { (proj2 a) where a is Element of C1 [*] C2 : a in A } ;

now

let a1, b1 be set ; :: thesis: ( a1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C1 )
assume a1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: ( b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C1 )
then consider a being Element of C1 [*] C2 such that
A3: ( a1 = proj1 a & a in A ) ;
assume b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: a1 \/ b1 in C1
then consider b being Element of C1 [*] C2 such that
A4: ( b1 = proj1 b & b in A ) ;
a \/ b in C1 [*] C2 by A2, A3, A4;
then proj1 (a \/ b) in C1 by Th98;
hence a1 \/ b1 in C1 by A3, A4, FUNCT_5:6; :: thesis: verum

end;

then A5: union { (proj1 a) where a is Element of C1 [*] C2 : a in A } in C1 by Def1;

now

let a1, b1 be set ; :: thesis: ( a1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C2 )
assume a1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: ( b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C2 )
then consider a being Element of C1 [*] C2 such that
A6: ( a1 = proj2 a & a in A ) ;
assume b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: a1 \/ b1 in C2
then consider b being Element of C1 [*] C2 such that
A7: ( b1 = proj2 b & b in A ) ;
a \/ b in C1 [*] C2 by A2, A6, A7;
then proj2 (a \/ b) in C2 by Th98;
hence a1 \/ b1 in C2 by A6, A7, FUNCT_5:6; :: thesis: verum

end;

then A8: union { (proj2 a) where a is Element of C1 [*] C2 : a in A } in C2 by Def1;
union A c= [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] )
assume x in union A ; :: thesis: x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):]
then consider a being set such that
A9: ( x in a & a in A ) by TARSKI:def 4;
a \/ a in C1 [*] C2 by A2, A9;
then ( a c= [:(proj1 a),(proj2 a):] & proj1 a in { (proj1 a) where a is Element of C1 [*] C2 : a in A } & proj2 a in { (proj2 a) where a is Element of C1 [*] C2 : a in A } ) by A9, Th98;
then A10: ( x in [:(proj1 a),(proj2 a):] & proj1 a c= union { (proj1 a) where a is Element of C1 [*] C2 : a in A } & proj2 a c= union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ) by A9, ZFMISC_1:92;
then [:(proj1 a),(proj2 a):] c= [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] by ZFMISC_1:119;
hence x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] by A10; :: thesis: verum

end;

hence union A in C1 [*] C2 by A5, A8, Th97; :: thesis: verum