let C1, C2 be Coherence_Space; for x, y being set holds
( [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 )
let x, y be set ; ( [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 )
A1:
( [[x,2],[y,2]] in Web (C1 "\/" C2) iff {[x,2],[y,2]} in C1 "\/" C2 )
by COH_SP:5;
A2:
( [x,y] in Web C2 iff {x,y} in C2 )
by COH_SP:5;
( {} U+ {x,y} = [:{x,y},{2}:] & [:{x,y},{2}:] = {[x,2],[y,2]} )
by Th74, ZFMISC_1:30;
hence
( [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 )
by A1, A2, Th86; verum