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