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 that
A1: {x,y} c= union C and
A2: not {x,y} in C ; :: thesis: {x,y} in 'not' C

now :: thesis: for a being Element of C ex z being set st {x,y} /\ a c= {z}

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
A3: ( ( 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 object ; :: according to TARSKI:def 3 :: thesis: ( not v in {x,y} /\ a or v in {z} )
assume A4: v in {x,y} /\ a ; :: thesis: v in {z}
then A5: v in {x,y} by XBOOLE_0:def 4;
A6: v in a by A4, XBOOLE_0:def 4;

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

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

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

end;

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

then ( x in a implies {x,y} c= a ) by A6, ZFMISC_1:32;
hence v in {z} by A2, A3, A7, CLASSES1:def 1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

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