let C be Coherence_Space; :: thesis: 'not' ('not' C) c= C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 'not' ('not' C) or x in C )
assume x in 'not' ('not' C) ; :: thesis: x in C
then consider a being Subset of (union ('not' C)) such that
A1: x = a and
A2: for b being Element of 'not' C ex x being set st a /\ b c= {x} ;
A3: union ('not' C) = union C by Th66;

now :: thesis: for x, y being set st x in a & y in a holds
{x,y} in C

let x, y be set ; :: thesis: ( x in a & y in a implies {x,y} in C )
assume that
A4: x in a and
A5: y in a and
A6: not {x,y} in C ; :: thesis: contradiction
{x,y} c= union C by A3, A4, A5, ZFMISC_1:32;
then {x,y} in 'not' C by A6, Th68;
then consider z being set such that
A7: a /\ {x,y} c= {z} by A2;
y in {x,y} by TARSKI:def 2;
then y in a /\ {x,y} by A5, XBOOLE_0:def 4;
then A8: y = z by A7, TARSKI:def 1;
x in {x,y} by TARSKI:def 2;
then x in a /\ {x,y} by A4, XBOOLE_0:def 4;
then x = z by A7, TARSKI:def 1;
then {x,y} = {x} by A8, ENUMSET1:29;
hence contradiction by A3, A4, A6, COH_SP:4; :: thesis: verum

end;

hence x in C by A1, COH_SP:6; :: thesis: verum