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) )
assume A1: x in 'not' (C1 "/\" C2) ; :: thesis: x in ('not' C1) "\/" ('not' C2)
then A2: ( x c= union (C1 "/\" C2) & ( for a being Element of C1 "/\" C2 ex z being set st x /\ a c= {z} ) ) by Th66;
union (C1 "/\" C2) = (union C1) U+ (union C2) by Th86;
then consider x1, x2 being set such that
A3: ( x = x1 U+ x2 & x1 c= union C1 & x2 c= union C2 ) by A2, Th80;

now

let a be Element of C1; :: thesis: ex z being set st x1 /\ a c= {z}
reconsider b = {} as Element of C2 by COH_SP:1;
a U+ b in C1 "/\" C2 ;
then consider z being set such that
A4: x /\ (a U+ b) c= {z} by A1, Th66;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A4, 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 A5: [:(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} )
assume A6: y in x1 /\ a ; :: thesis: y in {zz}
1 in {1} by TARSKI:def 1;
then ( [y,1] in [:(x1 /\ a),{1}:] & [z1,1] in [:(x1 /\ a),{1}:] ) by A6, ZFMISC_1:106;
then ( [y,1] = z & [z1,1] = z ) by A5, TARSKI:def 1;
then y = z1 by 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 A3, Th66;

now

let b be Element of C2; :: thesis: ex z being set st x2 /\ b c= {z}
reconsider a = {} as Element of C1 by COH_SP:1;
a U+ b in C1 "/\" C2 ;
then consider z being set such that
A7: x /\ (a U+ b) c= {z} by A1, Th66;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A7, 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 A8: [:(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} )
assume A9: y in x2 /\ b ; :: thesis: y in {zz}
2 in {2} by TARSKI:def 1;
then ( [y,2] in [:(x2 /\ b),{2}:] & [z1,2] in [:(x2 /\ b),{2}:] ) by A9, ZFMISC_1:106;
then ( [y,2] = z & [z1,2] = z ) by A8, TARSKI:def 1;
then y = z1 by 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 A3, 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' C1) = union C1 & union ('not' C2) = union C2 ) by Th67;
then ( y1 in union C1 & y2 in union C2 ) by TARSKI:def 4;
then ( {y1} in C1 & {y2} in C2 ) by COH_SP:4;
then {y1} U+ {y2} in C1 "/\" C2 ;
then consider z being set such that
A10: x /\ ({y1} U+ {y2}) c= {z} by A1, Th66;
( y1 in {y1} & y2 in {y2} ) by TARSKI:def 1;
then ( y1 in x1 /\ {y1} & y2 in x2 /\ {y2} ) by XBOOLE_0:def 4;
then ( (x1 /\ {y1}) U+ (x2 /\ {y2}) c= {z} & [y1,1] in (x1 /\ {y1}) U+ (x2 /\ {y2}) & [y2,2] in (x1 /\ {y1}) U+ (x2 /\ {y2}) ) by A3, A10, Th77, Th78, Th83;
then ( [y1,1] = z & [y2,2] = z & 1 <> 2 ) by TARSKI:def 1;
hence contradiction by 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
A11: ( x = x1 U+ x2 & ( x1 = {} or x2 = {} ) ) by Th88;
( x1 c= union ('not' C1) & x2 c= union ('not' C2) ) by ZFMISC_1:92;
then ( x1 c= union C1 & x2 c= union C2 ) by Th67;
then x c= (union C1) U+ (union C2) by A11, Th79;
then A12: x c= union (C1 "/\" C2) by Th86;
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
A13: a = a1 U+ a2 by Th84;
A14: x /\ a = (x1 /\ a1) U+ (x2 /\ a2) by A11, A13, Th83;
consider z1 being set such that
A15: x1 /\ a1 c= {z1} by Th66;
consider z2 being set such that
A16: x2 /\ a2 c= {z2} by Th66;
( x1 = {} or x1 <> {} ) ;
then consider z being set such that
A17: ( ( 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 y in x /\ a ; :: thesis: y in {z}
then A18: ( y = [(y `1 ),(y `2 )] & ( ( y `2 = 1 & y `1 in x1 /\ a1 ) or ( y `2 = 2 & y `1 in x2 /\ a2 ) ) ) by A14, Th76;

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

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

then y `1 = z2 by A16, A18, TARSKI:def 1;
hence y in {z} by A18, A19, TARSKI:def 1; :: thesis: verum

end;

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

then y `1 = z1 by A11, A15, A18, TARSKI:def 1;
hence y in {z} by A11, A18, A20, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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