let C1, C2 be Coherence_Space; :: thesis: union (C1 [*] C2) = [:(union C1),(union C2):]
thus union (C1 [*] C2) c= [:(union C1),(union C2):] :: according to XBOOLE_0:def 10 :: thesis: [:(union C1),(union C2):] c= union (C1 [*] C2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (C1 [*] C2) or x in [:(union C1),(union C2):] )
assume x in union (C1 [*] C2) ; :: thesis: x in [:(union C1),(union C2):]
then consider a being set such that
A1: x in a and
A2: a in C1 [*] C2 by TARSKI:def 4;
consider a1 being Element of C1, a2 being Element of C2 such that
A3: a c= [:a1,a2:] by A2, Th96;
( a1 c= union C1 & a2 c= union C2 ) by ZFMISC_1:74;
then [:a1,a2:] c= [:(union C1),(union C2):] by ZFMISC_1:96;
then a c= [:(union C1),(union C2):] by A3;
hence x in [:(union C1),(union C2):] by A1; :: thesis: verum

end;

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in [:(union C1),(union C2):] or [x,y] in union (C1 [*] C2) )
assume A4: [x,y] in [:(union C1),(union C2):] ; :: thesis: [x,y] in union (C1 [*] C2)
then x in union C1 by ZFMISC_1:87;
then consider a1 being set such that
A5: x in a1 and
A6: a1 in C1 by TARSKI:def 4;
y in union C2 by A4, ZFMISC_1:87;
then consider a2 being set such that
A7: y in a2 and
A8: a2 in C2 by TARSKI:def 4;
A9: [:a1,a2:] in C1 [*] C2 by A6, A8, Th96;
[x,y] in [:a1,a2:] by A5, A7, ZFMISC_1:87;
hence [x,y] in union (C1 [*] C2) by A9, TARSKI:def 4; :: thesis: verum