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 that
A1: x <> y and
A2: ( {x,y} in C & {x,y} in 'not' C ) ; :: thesis: contradiction
consider z being set such that
A3: {x,y} /\ {x,y} c= {z} by A2, Th65;
x = z by A3, ZFMISC_1:20;
hence contradiction by A1, A3, ZFMISC_1:20; :: thesis: verum