let C be Coherence_Space; 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 ; ( {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
; {x,y} in 'not' C
hence
{x,y} in 'not' C
by A1; verum