let C be Coherence_Space; :: thesis: union ('not' C) = union C

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: union C c= union ('not' C)

let x be object ; :: thesis: ( x in union ('not' C) implies x in union C )
assume x in union ('not' C) ; :: thesis: x in union C
then consider a being set such that
A1: x in a and
A2: a in 'not' C by TARSKI:def 4;
a c= union C by A2, Th65;
hence x in union C by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union C or x in union ('not' C) )
assume x in union C ; :: thesis: x in union ('not' C)
then A3: {x} c= union C by ZFMISC_1:31;
for a being Element of C ex z being set st {x} /\ a c= {z}

proof

let a be Element of C; :: thesis: ex z being set st {x} /\ a c= {z}
consider z being object such that
A4: {x} /\ a c= {z} by XBOOLE_1:17;
reconsider z = z as set by TARSKI:1;
take z ; :: thesis: {x} /\ a c= {z}
thus {x} /\ a c= {z} by A4; :: thesis: verum

end;

then ( x in {x} & {x} in 'not' C ) by A3, ZFMISC_1:31;
hence x in union ('not' C) by TARSKI:def 4; :: thesis: verum