let C be Coherence_Space; 'not' ('not' C) c= C
let x be object ; TARSKI:def 3 ( not x in 'not' ('not' C) or x in C )
assume
x in 'not' ('not' C)
; 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 for x, y being set st x in a & y in a holds
{x,y} in Clet x,
y be
set ;
( 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
;
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;
verum end;
hence
x in C
by A1, COH_SP:6; verum