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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in 'not' (C1 "/\" C2) or x in ('not' C1) "\/" ('not' C2) )
reconsider xx = x as set by TARSKI:1;
A1: union (C1 "/\" C2) = (union C1) U+ (union C2) by Th85;
assume A2: x in 'not' (C1 "/\" C2) ; :: thesis: x in ('not' C1) "\/" ('not' C2)
then xx c= union (C1 "/\" C2) by Th65;
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, Th79;
now :: thesis: for a being Element of C1 ex z being set st x1 /\ a c= {z}
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: xx /\ (a U+ b) c= {z} by A2, Th65;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A6, Th82;
then ( [:(x1 /\ a),{1}:] c= [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] & [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] c= {z} ) by Th73, XBOOLE_1:7;
then A7: [:(x1 /\ a),{1}:] c= {z} ;
now :: thesis: ( ( x1 /\ a = {} implies x1 /\ a c= {0} ) & ( x1 /\ a <> {} implies ex zz being set st x1 /\ a c= {zz} ) )
thus ( x1 /\ a = {} implies x1 /\ a c= {0} ) ; :: 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 ;
set z1 = the Element of A;
reconsider zz = the Element of A as set ;
take zz = zz; :: thesis: x1 /\ a c= {zz}
thus x1 /\ a c= {zz} :: thesis: verum
proof
let y be object ; :: 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:87;
then A9: [y,1] = z by A7, TARSKI:def 1;
[ the Element of A,1] in [:(x1 /\ a),{1}:] by A8, ZFMISC_1:87;
then [ the Element of A,1] = z by A7, TARSKI:def 1;
then y = the Element of A by A9, XTUPLE_0:1;
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, Th65;
now :: thesis: for b being Element of C2 ex z being set st x2 /\ b c= {z}
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: xx /\ (a U+ b) c= {z} by A2, Th65;
(x1 /\ a) U+ (x2 /\ b) c= {z} by A3, A10, Th82;
then ( [:(x2 /\ b),{2}:] c= [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] & [:(x1 /\ a),{1}:] \/ [:(x2 /\ b),{2}:] c= {z} ) by Th73, XBOOLE_1:7;
then A11: [:(x2 /\ b),{2}:] c= {z} ;
now :: thesis: ( ( x2 /\ b = {} implies x2 /\ b c= {0} ) & ( x2 /\ b <> {} implies ex zz being set st x2 /\ b c= {zz} ) )
thus ( x2 /\ b = {} implies x2 /\ b c= {0} ) ; :: 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 ;
set z1 = the Element of A;
reconsider zz = the Element of A as set ;
take zz = zz; :: thesis: x2 /\ b c= {zz}
thus x2 /\ b c= {zz} :: thesis: verum
proof
let y be object ; :: 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:87;
then A13: [y,2] = z by A11, TARSKI:def 1;
[ the Element of A,2] in [:(x2 /\ b),{2}:] by A12, ZFMISC_1:87;
then [ the Element of A,2] = z by A11, TARSKI:def 1;
then y = the Element of A by A13, XTUPLE_0:1;
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, Th65;
now :: thesis: ( x1 in 'not' C1 & x2 in 'not' C2 & ( x1 <> {} implies not x2 <> {} ) )
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 ;
set y1 = the Element of x1;
set y2 = the Element of x2;
union ('not' C2) = union C2 by Th66;
then the Element of x2 in union C2 by TARSKI:def 4;
then A14: { the Element of x2} in C2 by COH_SP:4;
union ('not' C1) = union C1 by Th66;
then the Element of x1 in union C1 by TARSKI:def 4;
then { the Element of x1} in C1 by COH_SP:4;
then { the Element of x1} U+ { the Element of x2} in C1 "/\" C2 by A14;
then consider z being set such that
A15: xx /\ ({ the Element of x1} U+ { the Element of x2}) c= {z} by A2, Th65;
A16: (x1 /\ { the Element of x1}) U+ (x2 /\ { the Element of x2}) c= {z} by A3, A15, Th82;
the Element of x2 in { the Element of x2} by TARSKI:def 1;
then the Element of x2 in x2 /\ { the Element of x2} by XBOOLE_0:def 4;
then [ the Element of x2,2] in (x1 /\ { the Element of x1}) U+ (x2 /\ { the Element of x2}) by Th77;
then A17: [ the Element of x2,2] = z by A16, TARSKI:def 1;
the Element of x1 in { the Element of x1} by TARSKI:def 1;
then the Element of x1 in x1 /\ { the Element of x1} by XBOOLE_0:def 4;
then [ the Element of x1,1] in (x1 /\ { the Element of x1}) U+ (x2 /\ { the Element of x2}) by Th76;
then [ the Element of x1,1] = z by A16, TARSKI:def 1;
hence contradiction by A17, XTUPLE_0:1; :: thesis: verum
end;
hence x in ('not' C1) "\/" ('not' C2) by A3, Th86; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ('not' C1) "\/" ('not' C2) or x in 'not' (C1 "/\" C2) )
reconsider xx = x as set by TARSKI:1;
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 Th87;
A20: for a being Element of C1 "/\" C2 ex z being set st xx /\ a c= {z}
proof
let a be Element of C1 "/\" C2; :: thesis: ex z being set st xx /\ a c= {z}
consider a1 being Element of C1, a2 being Element of C2 such that
A21: a = a1 U+ a2 by Th83;
A22: xx /\ a = (x1 /\ a1) U+ (x2 /\ a2) by A18, A21, Th82;
consider z2 being set such that
A23: x2 /\ a2 c= {z2} by Th65;
consider z1 being set such that
A24: x1 /\ a1 c= {z1} by Th65;
( x1 = {} or x1 <> {} ) ;
then consider z being set such that
A25: ( ( z = [z2,2] & x1 = {} ) or ( z = [z1,1] & x1 <> {} ) ) ;
take z ; :: thesis: xx /\ a c= {z}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx /\ a or y in {z} )
assume A26: y in xx /\ a ; :: thesis: y in {z}
then A27: y = [(y `1),(y `2)] by A22, Th75;
A28: ( ( y `2 = 1 & y `1 in x1 /\ a1 ) or ( y `2 = 2 & y `1 in x2 /\ a2 ) ) by A22, A26, Th75;
per cases ( ( z = [z2,2] & x1 = {} ) or ( z = [z1,1] & x1 <> {} ) ) by A25;
end;
end;
x2 c= union ('not' C2) by ZFMISC_1:74;
then A31: x2 c= union C2 by Th66;
x1 c= union ('not' C1) by ZFMISC_1:74;
then x1 c= union C1 by Th66;
then xx c= (union C1) U+ (union C2) by A18, A31, Th78;
then xx c= union (C1 "/\" C2) by Th85;
hence x in 'not' (C1 "/\" C2) by A20; :: thesis: verum