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 ( x in a & y in a ) ; :: thesis: {x,y} in 'not' ('not' C)
then A3: ( {x,y} c= a & x in union C & y in union C ) by A1, TARSKI:def 4, ZFMISC_1:38;
then A4: ( {x,y} in C & {x,y} c= union C ) by A1, CLASSES1:def 1, ZFMISC_1:38;
then ( x <> y implies not {x,y} in 'not' C ) by Th68;
then ( ( x <> y implies {x,y} in 'not' ('not' C) ) & {x,x} = {x} & ( x <> y or x = y ) ) by A2, A4, Th69, ENUMSET1:69;
hence {x,y} in 'not' ('not' C) by A2, A3, COH_SP:4; :: thesis: verum

end;

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