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 set ; :: 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 & a in 'not' C ) by TARSKI:def 4;
a c= union C by A1, Th66;
hence x in union C by A1; :: thesis: verum

end;

let x be set ; :: 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 A2: ( {x} c= union C & x in {x} ) by ZFMISC_1:37;
for a being Element of C ex z being set st {x} /\ a c= {z} by XBOOLE_1:17;
then {x} in 'not' C by A2;
hence x in union ('not' C) by A2, TARSKI:def 4; :: thesis: verum