let C1, C2 be Coherence_Space; :: thesis: for x, y being set st x in union C1 & y in union C2 holds
( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) )
let x, y be set ; :: thesis: ( x in union C1 & y in union C2 implies ( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) ) )
assume ( x in union C1 & y in union C2 ) ; :: thesis: ( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) )
then ( {x} in C1 & {y} in C2 ) by COH_SP:4;
then {x} U+ {y} in C1 "/\" C2 ;
then [:{x},{1}:] \/ [:{y},{2}:] in C1 "/\" C2 by Th73;
then {[x,1]} \/ [:{y},{2}:] in C1 "/\" C2 by ZFMISC_1:29;
then {[x,1]} \/ {[y,2]} in C1 "/\" C2 by ZFMISC_1:29;
then A1: {[x,1],[y,2]} in C1 "/\" C2 by ENUMSET1:1;
hence [[x,1],[y,2]] in Web (C1 "/\" C2) by COH_SP:5; :: thesis: [[y,2],[x,1]] in Web (C1 "/\" C2)
thus [[y,2],[x,1]] in Web (C1 "/\" C2) by A1, COH_SP:5; :: thesis: verum