let C1, C2 be Coherence_Space; :: thesis: 'not' (C1 "/\" C2) = ('not' C1) "\/" ('not' C2)
set C = C1 "/\" C2;
thus 'not' (C1 "/\" C2) c= ('not' C1) "\/" ('not' C2) :: according to XBOOLE_0:def 10 :: thesis: ('not' C1) "\/" ('not' C2) c= 'not' (C1 "/\" C2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 'not' (C1 "/\" C2) or x in ('not' C1) "\/" ('not' C2) )
A1: union (C1 "/\" C2) = (union C1) U+ (union C2) by Th86;
assume A2: x in 'not' (C1 "/\" C2) ; :: thesis: x in ('not' C1) "\/" ('not' C2)
then x c= union (C1 "/\" C2) by Th66;
then consider x1, x2 being set such that
A3: x = x1 U+ x2 and
A4: x1 c= union C1 and
A5: x2 c= union C2 by A1, Th80;

now

reconsider b = {} as Element of C2 by COH_SP:1;
let a be Element of C1; :: thesis: ex z being set st x1 /\ a c= {z}
a U+ b in C1 "/\" C2 ;
then consider z being set such that
A6: x /\ (a U+ b) c= {z} by A2, Th66;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A6, Th83;
then ( [:(x1 /\ a),{1}:] c= [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] & [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] c= {z} ) by Th74, XBOOLE_1:7;
then A7: [:(x1 /\ a),{1}:] c= {z} by XBOOLE_1:1;

now

thus ( x1 /\ a = {} implies x1 /\ a c= {0 } ) by XBOOLE_1:2; :: thesis: ( x1 /\ a <> {} implies ex zz being set st x1 /\ a c= {zz} )
assume x1 /\ a <> {} ; :: thesis: ex zz being set st x1 /\ a c= {zz}
then reconsider A = x1 /\ a as non empty set ;
consider z1 being Element of A;
reconsider zz = z1 as set ;
take zz = zz; :: thesis: x1 /\ a c= {zz}
thus x1 /\ a c= {zz} :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x1 /\ a or y in {zz} )
A8: 1 in {1} by TARSKI:def 1;
assume y in x1 /\ a ; :: thesis: y in {zz}
then [y,1] in [:(x1 /\ a),{1}:] by A8, ZFMISC_1:106;
then A9: [y,1] = z by A7, TARSKI:def 1;
[z1,1] in [:(x1 /\ a),{1}:] by A8, ZFMISC_1:106;
then [z1,1] = z by A7, TARSKI:def 1;
then y = z1 by A9, ZFMISC_1:33;
hence y in {zz} by TARSKI:def 1; :: thesis: verum

end;

end;

hence ex z being set st x1 /\ a c= {z} ; :: thesis: verum

end;

then reconsider x1 = x1 as Element of 'not' C1 by A4, Th66;

now

reconsider a = {} as Element of C1 by COH_SP:1;
let b be Element of C2; :: thesis: ex z being set st x2 /\ b c= {z}
a U+ b in C1 "/\" C2 ;
then consider z being set such that
A10: x /\ (a U+ b) c= {z} by A2, Th66;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A10, Th83;
then ( [:(x2 /\ b),{2}:] c= [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] & [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] c= {z} ) by Th74, XBOOLE_1:7;
then A11: [:(x2 /\ b),{2}:] c= {z} by XBOOLE_1:1;

now

thus ( x2 /\ b = {} implies x2 /\ b c= {0 } ) by XBOOLE_1:2; :: thesis: ( x2 /\ b <> {} implies ex zz being set st x2 /\ b c= {zz} )
assume x2 /\ b <> {} ; :: thesis: ex zz being set st x2 /\ b c= {zz}
then reconsider A = x2 /\ b as non empty set ;
consider z1 being Element of A;
reconsider zz = z1 as set ;
take zz = zz; :: thesis: x2 /\ b c= {zz}
thus x2 /\ b c= {zz} :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x2 /\ b or y in {zz} )
A12: 2 in {2} by TARSKI:def 1;
assume y in x2 /\ b ; :: thesis: y in {zz}
then [y,2] in [:(x2 /\ b),{2}:] by A12, ZFMISC_1:106;
then A13: [y,2] = z by A11, TARSKI:def 1;
[z1,2] in [:(x2 /\ b),{2}:] by A12, ZFMISC_1:106;
then [z1,2] = z by A11, TARSKI:def 1;
then y = z1 by A13, ZFMISC_1:33;
hence y in {zz} by TARSKI:def 1; :: thesis: verum

end;

end;

hence ex z being set st x2 /\ b c= {z} ; :: thesis: verum

end;

then reconsider x2 = x2 as Element of 'not' C2 by A5, Th66;

now

thus ( x1 in 'not' C1 & x2 in 'not' C2 ) ; :: thesis: ( x1 <> {} implies not x2 <> {} )
assume ( x1 <> {} & x2 <> {} ) ; :: thesis: contradiction
then reconsider x1 = x1, x2 = x2 as non empty set ;
consider y1 being Element of x1, y2 being Element of x2;
union ('not' C2) = union C2 by Th67;
then y2 in union C2 by TARSKI:def 4;
then A14: {y2} in C2 by COH_SP:4;
union ('not' C1) = union C1 by Th67;
then y1 in union C1 by TARSKI:def 4;
then {y1} in C1 by COH_SP:4;
then {y1} U+ {y2} in C1 "/\" C2 by A14;
then consider z being set such that
A15: x /\ ({y1} U+ {y2}) c= {z} by A2, Th66;
A16: (x1 /\ {y1}) U+ (x2 /\ {y2}) c= {z} by A3, A15, Th83;
y2 in {y2} by TARSKI:def 1;
then y2 in x2 /\ {y2} by XBOOLE_0:def 4;
then [y2,2] in (x1 /\ {y1}) U+ (x2 /\ {y2}) by Th78;
then A17: [y2,2] = z by A16, TARSKI:def 1;
y1 in {y1} by TARSKI:def 1;
then y1 in x1 /\ {y1} by XBOOLE_0:def 4;
then [y1,1] in (x1 /\ {y1}) U+ (x2 /\ {y2}) by Th77;
then [y1,1] = z by A16, TARSKI:def 1;
hence contradiction by A17, ZFMISC_1:33; :: thesis: verum

end;

hence x in ('not' C1) "\/" ('not' C2) by A3, Th87; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ('not' C1) "\/" ('not' C2) or x in 'not' (C1 "/\" C2) )
assume x in ('not' C1) "\/" ('not' C2) ; :: thesis: x in 'not' (C1 "/\" C2)
then consider x1 being Element of 'not' C1, x2 being Element of 'not' C2 such that
A18: x = x1 U+ x2 and
A19: ( x1 = {} or x2 = {} ) by Th88;
A20: for a being Element of C1 "/\" C2 ex z being set st x /\ a c= {z}

proof

let a be Element of C1 "/\" C2; :: thesis: ex z being set st x /\ a c= {z}
consider a1 being Element of C1, a2 being Element of C2 such that
A21: a = a1 U+ a2 by Th84;
A22: x /\ a = (x1 /\ a1) U+ (x2 /\ a2) by A18, A21, Th83;
consider z2 being set such that
A23: x2 /\ a2 c= {z2} by Th66;
consider z1 being set such that
A24: x1 /\ a1 c= {z1} by Th66;
( x1 = {} or x1 <> {} ) ;
then consider z being set such that
A25: ( ( z = [z2,2] & x1 = {} ) or ( z = [z1,1] & x1 <> {} ) ) ;
take z ; :: thesis: x /\ a c= {z}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x /\ a or y in {z} )
assume A26: y in x /\ a ; :: thesis: y in {z}
then A27: y = [(y `1 ),(y `2 )] by A22, Th76;
A28: ( ( y `2 = 1 & y `1 in x1 /\ a1 ) or ( y `2 = 2 & y `1 in x2 /\ a2 ) ) by A22, A26, Th76;

per cases ( ( z = [z2,2] & x1 = {} ) or ( z = [z1,1] & x1 <> {} ) ) by A25;

suppose A29: ( z = [z2,2] & x1 = {} ) ; :: thesis: y in {z}

then y `1 = z2 by A23, A28, TARSKI:def 1;
hence y in {z} by A27, A28, A29, TARSKI:def 1; :: thesis: verum

end;

suppose A30: ( z = [z1,1] & x1 <> {} ) ; :: thesis: y in {z}

then y `1 = z1 by A19, A24, A28, TARSKI:def 1;
hence y in {z} by A19, A27, A28, A30, TARSKI:def 1; :: thesis: verum

end;

end;

end;

x2 c= union ('not' C2) by ZFMISC_1:92;
then A31: x2 c= union C2 by Th67;
x1 c= union ('not' C1) by ZFMISC_1:92;
then x1 c= union C1 by Th67;
then x c= (union C1) U+ (union C2) by A18, A31, Th79;
then x c= union (C1 "/\" C2) by Th86;
hence x in 'not' (C1 "/\" C2) by A20; :: thesis: verum