let C1, C2 be Coherence_Space; :: thesis: for x, y being set holds
( not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2) )
let x, y be set ; :: thesis: ( not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2) )
A1: not {x} U+ {y} in C1 "\/" C2 by Th87;
A2: {x} U+ {y} = [:{x},{1}:] \/ [:{y},{2}:] by Th74
.= {[x,1]} \/ [:{y},{2}:] by ZFMISC_1:35
.= {[x,1]} \/ {[y,2]} by ZFMISC_1:35
.= {[x,1],[y,2]} by ENUMSET1:41 ;
hence not [[x,1],[y,2]] in Web (C1 "\/" C2) by A1, COH_SP:5; :: thesis: not [[y,2],[x,1]] in Web (C1 "\/" C2)
thus not [[y,2],[x,1]] in Web (C1 "\/" C2) by A1, A2, COH_SP:5; :: thesis: verum