let C1, C2 be Coherence_Space; :: thesis: 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 ; :: thesis: ( [[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;
A3: ( {} U+ {x,y} = [:{x,y},{2}:] & {} in C1 ) by Th75, COH_SP:1;
[:{x,y},{2}:] = {[x,2],[y,2]} by ZFMISC_1:36;
hence ( [[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2 ) by A1, A2, A3, Th85; :: thesis: verum