let C be Coherence_Space; :: thesis: for x, y being set st {x,y} c= union C & not {x,y} in C holds
{x,y} in 'not' C
let x, y be set ; :: thesis: ( {x,y} c= union C & not {x,y} in C implies {x,y} in 'not' C )
assume A1: ( {x,y} c= union C & not {x,y} in C ) ; :: thesis: {x,y} in 'not' C

now

let a be Element of C; :: thesis: ex z being set st {x,y} /\ a c= {z}
( x in a or not x in a ) ;
then consider z being set such that
A2: ( ( x in a & z = x ) or ( not x in a & z = y ) ) ;
take z = z; :: thesis: {x,y} /\ a c= {z}
thus {x,y} /\ a c= {z} :: thesis: verum

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in {x,y} /\ a or v in {z} )
assume A3: v in {x,y} /\ a ; :: thesis: v in {z}
then A4: ( v in {x,y} & v in a ) by XBOOLE_0:def 4;

per cases ( v = x or v = y ) by A4, TARSKI:def 2;

suppose v = x ; :: thesis: v in {z}

hence v in {z} by A2, A3, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A5: v = y ; :: thesis: v in {z}

then ( x in a implies {x,y} c= a ) by A4, ZFMISC_1:38;
hence v in {z} by A1, A2, A5, CLASSES1:def 1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

hence {x,y} in 'not' C by A1; :: thesis: verum