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 & {x,y} in C implies not {x,y} in 'not' C ) by Th68;
A2: ( {x,y} c= union C & not {x,y} in C implies {x,y} in 'not' C ) by Th69;
A3: union ('not' C) = union 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 A1, COH_SP:5, ZFMISC_1:106; :: 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 ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) ; :: thesis: [x,y] in Web ('not' C)
then ( {x,y} c= union C & ( ( x = y & {x} in 'not' C & {x} = {x,y} ) or not {x,y} in C ) ) by A3, COH_SP:4, COH_SP:5, ENUMSET1:69, ZFMISC_1:38;
hence [x,y] in Web ('not' C) by A2, COH_SP:5; :: thesis: verum