let C1, C2 be Coherence_Space; :: thesis: for a, b being finite Element of C1
for y1, y2 being set holds
( [[a,y1],[b,y2]] in Web (StabCoh C1,C2) iff ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) )
let a, b be finite Element of C1; :: thesis: for y1, y2 being set holds
( [[a,y1],[b,y2]] in Web (StabCoh C1,C2) iff ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) )
let y1, y2 be set ; :: thesis: ( [[a,y1],[b,y2]] in Web (StabCoh C1,C2) iff ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) )

hereby :: thesis: ( ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) implies [[a,y1],[b,y2]] in Web (StabCoh C1,C2) )

assume [[a,y1],[b,y2]] in Web (StabCoh C1,C2) ; :: thesis: ( ( a \/ b in C1 or not y1 in union C2 or not y2 in union C2 ) implies ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) )
then {[a,y1],[b,y2]} in StabCoh C1,C2 by COH_SP:5;
then consider f being U-stable Function of C1,C2 such that
A1: {[a,y1],[b,y2]} = Trace f by Def19;
A2: ( [a,y1] in {[a,y1],[b,y2]} & [b,y2] in {[a,y1],[b,y2]} ) by TARSKI:def 2;
assume A3: ( a \/ b in C1 or not y1 in union C2 or not y2 in union C2 ) ; :: thesis: ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) )
then {y1,y2} in C2 by A1, A2, Th35, ZFMISC_1:106;
hence [y1,y2] in Web C2 by COH_SP:5; :: thesis: ( y1 = y2 implies a = b )
thus ( y1 = y2 implies a = b ) by A1, A2, A3, Th36, ZFMISC_1:106; :: thesis: verum

end;

assume A4: ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) ; :: thesis: [[a,y1],[b,y2]] in Web (StabCoh C1,C2)
then A5: ( y1 in union C2 & y2 in union C2 & ( not a \/ b in C1 or ( {y1,y2} in C2 & ( y1 = y2 implies a = b ) ) ) ) by COH_SP:5, ZFMISC_1:106;
then ( [a,y1] in [:C1,(union C2):] & [b,y2] in [:C1,(union C2):] ) by ZFMISC_1:106;
then reconsider X = {[a,y1],[b,y2]} as Subset of [:C1,(union C2):] by ZFMISC_1:38;

A6: now

let x be set ; :: thesis: ( x in X implies x `1 is finite )
assume x in X ; :: thesis: x `1 is finite
then ( x = [a,y1] or x = [b,y2] ) by TARSKI:def 2;
hence x `1 is finite by MCART_1:7; :: thesis: verum

end;

A7: now

let a1, b1 be Element of C1; :: thesis: ( a1 \/ b1 in C1 implies for z1, z2 being set st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2 )
assume A8: a1 \/ b1 in C1 ; :: thesis: for z1, z2 being set st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2
let z1, z2 be set ; :: thesis: ( [a1,z1] in X & [b1,z2] in X implies {z1,z2} in C2 )
assume ( [a1,z1] in X & [b1,z2] in X ) ; :: thesis: {z1,z2} in C2
then ( ( [a1,z1] = [a,y1] or [a1,z1] = [b,y2] ) & ( [b1,z2] = [a,y1] or [b1,z2] = [b,y2] ) ) by TARSKI:def 2;
then ( ( ( z1 = y1 & a1 = a ) or ( a1 = b & z1 = y2 ) ) & {z1,z2} = {z2,z1} & ( ( z2 = y1 & b1 = a ) or ( b1 = b & z2 = y2 ) ) ) by ZFMISC_1:33;
then ( {z1,z2} = {y1} or {z1,z2} in C2 or {z1,z2} = {y2} ) by A4, A8, COH_SP:5, ENUMSET1:69;
hence {z1,z2} in C2 by A5, COH_SP:4; :: thesis: verum

end;

now

let a1, b1 be Element of C1; :: thesis: ( a1 \/ b1 in C1 implies for y being set st [a1,y] in X & [b1,y] in X holds
a1 = b1 )
assume A9: a1 \/ b1 in C1 ; :: thesis: for y being set st [a1,y] in X & [b1,y] in X holds
a1 = b1
let y be set ; :: thesis: ( [a1,y] in X & [b1,y] in X implies a1 = b1 )
assume ( [a1,y] in X & [b1,y] in X ) ; :: thesis: a1 = b1
then ( ( [a1,y] = [a,y1] or [a1,y] = [b,y2] ) & ( [b1,y] = [a,y1] or [b1,y] = [b,y2] ) ) by TARSKI:def 2;
then ( ( ( a1 = a & y = y1 ) or ( a1 = b & y = y2 ) ) & ( ( b1 = a & y = y1 ) or ( b1 = b & y = y2 ) ) ) by ZFMISC_1:33;
hence a1 = b1 by A4, A9; :: thesis: verum

end;

then ex f being U-stable Function of C1,C2 st X = Trace f by A6, A7, Th39;
then X in StabCoh C1,C2 by Def19;
hence [[a,y1],[b,y2]] in Web (StabCoh C1,C2) by COH_SP:5; :: thesis: verum