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 Def21;
( [x1,y1] in LinTrace f & [x2,y2] in LinTrace f ) by A1, TARSKI:def 2;
then ( [{x1},y1] in Trace f & [{x2},y2] in Trace f ) by Th51;
then A2: ( {x1} in dom f & {x2} in dom f & dom f = C1 & x1 in {x1} & x2 in {x2} & {[{x1},y1],[{x2},y2]} c= Trace f & Trace f in StabCoh C1,C2 ) by Def19, Th32, FUNCT_2:def 1, TARSKI:def 1, ZFMISC_1:38;
then ( x1 in union C1 & x2 in union C1 & {[{x1},y1],[{x2},y2]} in StabCoh C1,C2 ) by CLASSES1:def 1, TARSKI:def 4;
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 A2, Th49;
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:41, ZFMISC_1:6;
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 A2, 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:41;
then [[a,y1],[b,y2]] in Web (StabCoh C1,C2) by Th49;
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
A3: {[a,y1],[b,y2]} = Trace f by Def19;

now

let a1, y be set ; :: 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 A3, TARSKI:def 2;
then ( a1 = {x1} or a1 = {x2} ) by ZFMISC_1:33;
hence ex x being set st a1 = {x} ; :: thesis: verum

end;

then f is U-linear by Th50;
then A4: LinTrace f in LinCoh C1,C2 by Def21;
{[x1,y1],[x2,y2]} c= LinTrace f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[x1,y1],[x2,y2]} or x in LinTrace f )
assume x in {[x1,y1],[x2,y2]} ; :: thesis: x in LinTrace f
then ( ( x = [x1,y1] & [a,y1] in Trace f ) or ( x = [x2,y2] & [b,y2] in Trace f ) ) by A3, TARSKI:def 2;
hence x in LinTrace f by Th51; :: thesis: verum

end;

then {[x1,y1],[x2,y2]} in LinCoh C1,C2 by A4, CLASSES1:def 1;
hence [[x1,y1],[x2,y2]] in Web (LinCoh C1,C2) by COH_SP:5; :: thesis: verum