let C be Coherence_Space; :: thesis: for x, y being set st x <> y & {x,y} in C holds
not {x,y} in 'not' C
let x, y be set ; :: thesis: ( x <> y & {x,y} in C implies not {x,y} in 'not' C )
assume A1: ( x <> y & {x,y} in C & {x,y} in 'not' C ) ; :: thesis: contradiction
then consider z being set such that
A2: {x,y} /\ {x,y} c= {z} by Th66;
( x = z & y = z ) by A2, ZFMISC_1:26;
hence contradiction by A1; :: thesis: verum