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 object ; :: 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 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 = a1 U+ a2 and
( a1 = {} or a2 = {} ) by A2, Th87;
( a1 c= union C1 & a2 c= union C2 ) by ZFMISC_1:74;
then a c= (union C1) U+ (union C2) by A3, Th78;
hence x in (union C1) U+ (union C2) by A1; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (union C1) U+ (union C2) or z in union (C1 "\/" C2) )
assume A4: z in (union C1) U+ (union C2) ; :: thesis: z in union (C1 "\/" C2)
then A5: z = [(z `1),(z `2)] by Th75;
per cases ( ( z `2 = 1 & z `1 in union C1 ) or ( z `2 = 2 & z `1 in union C2 ) ) by A4, Th75;
suppose A6: ( z `2 = 1 & z `1 in union C1 ) ; :: thesis: z in union (C1 "\/" C2)
reconsider b = {} as Element of C2 by COH_SP:1;
consider a being set such that
A7: z `1 in a and
A8: a in C1 by A6, TARSKI:def 4;
reconsider a = a as Element of C1 by A8;
A9: a U+ b in C1 "\/" C2 by Th86;
z in a U+ b by A5, A6, A7, Th76;
hence z in union (C1 "\/" C2) by A9, TARSKI:def 4; :: thesis: verum
end;
suppose A10: ( z `2 = 2 & z `1 in union C2 ) ; :: thesis: z in union (C1 "\/" C2)
reconsider b = {} as Element of C1 by COH_SP:1;
consider a being set such that
A11: z `1 in a and
A12: a in C2 by A10, TARSKI:def 4;
reconsider a = a as Element of C2 by A12;
A13: b U+ a in C1 "\/" C2 by Th86;
z in b U+ a by A5, A10, A11, Th77;
hence z in union (C1 "\/" C2) by A13, TARSKI:def 4; :: thesis: verum
end;
end;