let C be Coherence_Space; :: thesis: for x, y being set holds
( [x,y] in Web ('not' C) iff ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) )
let x, y be set ; :: thesis: ( [x,y] in Web ('not' C) iff ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) )
A1: ( {x,y} c= union C & not {x,y} in C implies {x,y} in 'not' C ) by Th68;
A2: union ('not' C) = union C by Th66;
( x <> y & {x,y} in C implies not {x,y} in 'not' C ) by Th67;
hence ( [x,y] in Web ('not' C) implies ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) ) by A2, COH_SP:5, ZFMISC_1:87; :: thesis: ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) implies [x,y] in Web ('not' C) )
assume that
A3: x in union C and
A4: y in union C and
A5: ( x = y or not [x,y] in Web C ) ; :: thesis: [x,y] in Web ('not' C)
( ( x = y & {x} in 'not' C & {x} = {x,y} ) or not {x,y} in C ) by A2, A3, A5, COH_SP:4, COH_SP:5, ENUMSET1:29;
hence [x,y] in Web ('not' C) by A1, A3, A4, COH_SP:5, ZFMISC_1:32; :: thesis: verum