let C be Coherence_Space; :: thesis: 'not' ('not' C) = C
thus 'not' ('not' C) c= C by Lm7; :: according to XBOOLE_0:def 10 :: thesis: C c= 'not' ('not' C)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in C or a in 'not' ('not' C) )
assume A1: a in C ; :: thesis: a in 'not' ('not' C)
A2: ( union C = union ('not' C) & union ('not' C) = union ('not' ('not' C)) ) by Th67;

now

let x, y be set ; :: thesis: ( x in a & y in a implies {x,y} in 'not' ('not' C) )
assume that
A3: x in a and
A4: y in a ; :: thesis: {x,y} in 'not' ('not' C)
A5: x in union C by A1, A3, TARSKI:def 4;
{x,y} c= a by A3, A4, ZFMISC_1:32;
then {x,y} in C by A1, CLASSES1:def 1;
then A6: ( x <> y implies not {x,y} in 'not' C ) by Th68;
y in union C by A1, A4, TARSKI:def 4;
then A7: {x,y} c= union C by A5, ZFMISC_1:32;
{x,x} = {x} by ENUMSET1:29;
hence {x,y} in 'not' ('not' C) by A2, A5, A7, A6, Th69, COH_SP:4; :: thesis: verum

end;

hence a in 'not' ('not' C) by COH_SP:6; :: thesis: verum