let C1, C2 be Coherence_Space; :: thesis: for x1, x2, y1, y2 being set holds
( [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) iff ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ) )
let x1, x2, y1, y2 be set ; :: thesis: ( [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) iff ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ) )
hereby :: thesis: ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) implies [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) )
assume [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) ; :: thesis: ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) )
then {[x1,y1],[x2,y2]} in LinCoh (C1,C2) by COH_SP:5;
then consider f being U-linear Function of C1,C2 such that
A1: {[x1,y1],[x2,y2]} = LinTrace f by Def20;
[x1,y1] in LinTrace f by A1, TARSKI:def 2;
then A2: [{x1},y1] in Trace f by Th50;
then A3: {x1} in dom f by Th31;
[x2,y2] in LinTrace f by A1, TARSKI:def 2;
then A4: [{x2},y2] in Trace f by Th50;
then A5: {x2} in dom f by Th31;
A6: ( x1 in {x1} & x2 in {x2} ) by TARSKI:def 1;
A7: Trace f in StabCoh (C1,C2) by Def18;
A8: dom f = C1 by FUNCT_2:def 1;
{[{x1},y1],[{x2},y2]} c= Trace f by A2, A4, ZFMISC_1:32;
then {[{x1},y1],[{x2},y2]} in StabCoh (C1,C2) by A7, CLASSES1:def 1;
then [[{x1},y1],[{x2},y2]] in Web (StabCoh (C1,C2)) by COH_SP:5;
then ( ( not {x1} \/ {x2} in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies {x1} = {x2} ) ) ) by A3, A5, A8, Th48;
then ( ( not {x1,x2} in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) by ENUMSET1:1, ZFMISC_1:3;
hence ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ) by A3, A5, A8, A6, COH_SP:5, TARSKI:def 4; :: thesis: verum
end;
assume ( x1 in union C1 & x2 in union C1 ) ; :: thesis: ( ( not ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) & not ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) or [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) )
then reconsider a = {x1}, b = {x2} as Element of C1 by COH_SP:4;
assume ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ; :: thesis: [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2))
then ( ( not {x1,x2} in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) by COH_SP:5;
then ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) by ENUMSET1:1;
then [[a,y1],[b,y2]] in Web (StabCoh (C1,C2)) by Th48;
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
A9: {[a,y1],[b,y2]} = Trace f by Def18;
now :: thesis: for a1 being set
for y being object st [a1,y] in Trace f holds
ex x being set st a1 = {x}
let a1 be set ; :: thesis: for y being object st [a1,y] in Trace f holds
ex x being set st a1 = {x}
let y be object ; :: thesis: ( [a1,y] in Trace f implies ex x being set st a1 = {x} )
assume [a1,y] in Trace f ; :: thesis: ex x being set st a1 = {x}
then ( [a1,y] = [a,y1] or [a1,y] = [b,y2] ) by A9, TARSKI:def 2;
then ( a1 = {x1} or a1 = {x2} ) by XTUPLE_0:1;
hence ex x being set st a1 = {x} ; :: thesis: verum
end;
then f is U-linear by Th49;
then A10: LinTrace f in LinCoh (C1,C2) by Def20;
{[x1,y1],[x2,y2]} c= LinTrace f
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in {[x1,y1],[x2,y2]} or [x,y] in LinTrace f )
assume [x,y] in {[x1,y1],[x2,y2]} ; :: thesis: [x,y] in LinTrace f
then ( ( [x,y] = [x1,y1] & [a,y1] in Trace f ) or ( [x,y] = [x2,y2] & [b,y2] in Trace f ) ) by A9, TARSKI:def 2;
hence [x,y] in LinTrace f by Th50; :: thesis: verum
end;
then {[x1,y1],[x2,y2]} in LinCoh (C1,C2) by A10, CLASSES1:def 1;
hence [[x1,y1],[x2,y2]] in Web (LinCoh (C1,C2)) by COH_SP:5; :: thesis: verum