let C1, C2 be Coherence_Space; 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; 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 ; ( [[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 ( ( ( 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))
;
( ( 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 )
;
( [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;
( y1 = y2 implies a = b )thus
(
y1 = y2 implies
a = b )
by A1, A2, A3, Th35, ZFMISC_1:87;
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 ) ) )
; [[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 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 C2let a1,
b1 be
Element of
C1;
( 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
;
for z1, z2 being object st [a1,z1] in X & [b1,z2] in X holds
{z1,z2} in C2let z1,
z2 be
object ;
( [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
;
{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;
verum end;
A13:
now 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 = b1let a1,
b1 be
Element of
C1;
( 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
;
for y being object st [a1,y] in X & [b1,y] in X holds
a1 = b1let y be
object ;
( [a1,y] in X & [b1,y] in X implies a1 = b1 )assume that A15:
[a1,y] in X
and A16:
[b1,y] in X
;
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;
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; verum