let C1, C2 be Coherence_Space; :: thesis: union (C1 "\/" C2) = (union C1) U+ (union C2)
thus union (C1 "\/" C2) c= (union C1) U+ (union C2) :: according to XBOOLE_0:def 10 :: thesis: (union C1) U+ (union C2) c= union (C1 "\/" C2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (C1 "\/" C2) or x in (union C1) U+ (union C2) )
assume x in union (C1 "\/" C2) ; :: thesis: x in (union C1) U+ (union C2)
then consider a being set such that
A1: ( x in a & a in C1 "\/" C2 ) by TARSKI:def 4;
consider a1 being Element of C1, a2 being Element of C2 such that
A2: ( a = a1 U+ a2 & ( a1 = {} or a2 = {} ) ) by A1, Th88;
( a1 c= union C1 & a2 c= union C2 ) by ZFMISC_1:92;
then a c= (union C1) U+ (union C2) by A2, Th79;
hence x in (union C1) U+ (union C2) by A1; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (union C1) U+ (union C2) or z in union (C1 "\/" C2) )
assume A3: z in (union C1) U+ (union C2) ; :: thesis: z in union (C1 "\/" C2)
then A4: ( z = [(z `1 ),(z `2 )] & ( ( z `2 = 1 & z `1 in union C1 ) or ( z `2 = 2 & z `1 in union C2 ) ) ) by Th76;

per cases ( ( z `2 = 1 & z `1 in union C1 ) or ( z `2 = 2 & z `1 in union C2 ) ) by A3, Th76;

suppose A5: ( z `2 = 1 & z `1 in union C1 ) ; :: thesis: z in union (C1 "\/" C2)

then consider a being set such that
A6: ( z `1 in a & a in C1 ) by TARSKI:def 4;
reconsider a = a as Element of C1 by A6;
reconsider b = {} as Element of C2 by COH_SP:1;
( z in a U+ b & a U+ b in C1 "\/" C2 ) by A4, A5, A6, Th77, Th87;
hence z in union (C1 "\/" C2) by TARSKI:def 4; :: thesis: verum

end;

suppose A7: ( z `2 = 2 & z `1 in union C2 ) ; :: thesis: z in union (C1 "\/" C2)

then consider a being set such that
A8: ( z `1 in a & a in C2 ) by TARSKI:def 4;
reconsider a = a as Element of C2 by A8;
reconsider b = {} as Element of C1 by COH_SP:1;
( z in b U+ a & b U+ a in C1 "\/" C2 ) by A4, A7, A8, Th78, Th87;
hence z in union (C1 "\/" C2) by TARSKI:def 4; :: thesis: verum

end;

end;