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: {x} U+ {y} = [:{x},{1}:] \/ [:{y},{2}:] by Th73
.= {[x,1]} \/ [:{y},{2}:] by ZFMISC_1:29
.= {[x,1]} \/ {[y,2]} by ZFMISC_1:29
.= {[x,1],[y,2]} by ENUMSET1:1 ;
A2: not {x} U+ {y} in C1 "\/" C2 by Th86;
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 A2, A1, COH_SP:5; :: thesis: verum