let C be Coherence_Space; 'not' ('not' C) = C
thus
'not' ('not' C) c= C
by Lm7; XBOOLE_0:def 10 C c= 'not' ('not' C)
let a be object ; TARSKI:def 3 ( not a in C or a in 'not' ('not' C) )
reconsider aa = a as set by TARSKI:1;
assume A1:
a in C
; a in 'not' ('not' C)
A2:
( union C = union ('not' C) & union ('not' C) = union ('not' ('not' C)) )
by Th66;
now for x, y being set st x in aa & y in aa holds
{x,y} in 'not' ('not' C)let x,
y be
set ;
( x in aa & y in aa implies {x,y} in 'not' ('not' C) )assume that A3:
x in aa
and A4:
y in aa
;
{x,y} in 'not' ('not' C)A5:
x in union C
by A1, A3, TARSKI:def 4;
{x,y} c= aa
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 Th67;
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, Th68, COH_SP:4;
verum end;
hence
a in 'not' ('not' C)
by COH_SP:6; verum