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 A1: ex f being U-stable Function of C1,C2 st {[a,y1],[b,y2]} = Trace f by Def18;
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, Th34, ZFMISC_1:87;
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, Th35, ZFMISC_1:87; :: 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: y2 in union C2 by ZFMISC_1:87;
then A6: [b,y2] in [:C1,(union C2):] by ZFMISC_1:87;
A7: y1 in union C2 by A4, ZFMISC_1:87;
then [a,y1] in [:C1,(union C2):] by ZFMISC_1:87;
then reconsider X = {[a,y1],[b,y2]} as Subset of [:C1,(union C2):] by A6, ZFMISC_1:32;

A8: now :: thesis: for a1, b1 being Element of C1 st a1 \/ b1 in C1 holds
for z1, z2 being object st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2

let a1, b1 be Element of C1; :: thesis: ( a1 \/ b1 in C1 implies for z1, z2 being object st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2 )
assume A9: a1 \/ b1 in C1 ; :: thesis: for z1, z2 being object st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2
let z1, z2 be object ; :: thesis: ( [a1,z1] in X & [b1,z2] in X implies {z1,z2} in C2 )
assume that
A10: [a1,z1] in X and
A11: [b1,z2] in X ; :: thesis: {z1,z2} in C2
( [b1,z2] = [a,y1] or [b1,z2] = [b,y2] ) by A11, TARSKI:def 2;
then A12: ( ( z2 = y1 & b1 = a ) or ( b1 = b & z2 = y2 ) ) by XTUPLE_0:1;
( [a1,z1] = [a,y1] or [a1,z1] = [b,y2] ) by A10, TARSKI:def 2;
then ( ( z1 = y1 & a1 = a ) or ( a1 = b & z1 = y2 ) ) by XTUPLE_0:1;
then ( {z1,z2} = {y1} or {z1,z2} in C2 or {z1,z2} = {y2} ) by A4, A9, A12, COH_SP:5, ENUMSET1:29;
hence {z1,z2} in C2 by A7, A5, COH_SP:4; :: thesis: verum

end;

A13: now :: thesis: for a1, b1 being Element of C1 st a1 \/ b1 in C1 holds
for y being object st [a1,y] in X & [b1,y] in X holds
a1 = b1

let a1, b1 be Element of C1; :: thesis: ( a1 \/ b1 in C1 implies for y being object st [a1,y] in X & [b1,y] in X holds
a1 = b1 )
assume A14: a1 \/ b1 in C1 ; :: thesis: for y being object st [a1,y] in X & [b1,y] in X holds
a1 = b1
let y be object ; :: thesis: ( [a1,y] in X & [b1,y] in X implies a1 = b1 )
assume that
A15: [a1,y] in X and
A16: [b1,y] in X ; :: thesis: a1 = b1
( [a1,y] = [a,y1] or [a1,y] = [b,y2] ) by A15, TARSKI:def 2;
then A17: ( ( a1 = a & y = y1 ) or ( a1 = b & y = y2 ) ) by XTUPLE_0:1;
( [b1,y] = [a,y1] or [b1,y] = [b,y2] ) by A16, TARSKI:def 2;
hence a1 = b1 by A4, A14, A17, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for x being set st x in X holds
x `1 is finite

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 ; :: thesis: verum

end;

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