let G be Go-board; :: thesis: for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) & not ( i1 = i2 & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) & not ( i1 = i2 + 1 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
( i1 + 1 = i2 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} )
let i1, j1, i2, j2 be Nat; :: thesis: ( 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) & not ( i1 = i2 & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) & not ( i1 = i2 + 1 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) implies ( i1 + 1 = i2 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} ) )
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len G and
A3: ( 1 <= j1 & j1 <= width G ) and
A4: 1 <= i2 and
A5: i2 + 1 <= len G and
A6: ( 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) ; :: thesis: ( ( i1 = i2 & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) or ( i1 = i2 + 1 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) or ( i1 + 1 = i2 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} ) )
A7: j1 = j2 by A1, A2, A3, A4, A5, A6, Th20;
A8: (i1 + 1) + 1 = i1 + (1 + 1) ;
A9: (i2 + 1) + 1 = i2 + (1 + 1) ;
A10: ( |.(i1 - i2).| = 0 or |.(i1 - i2).| = 1 ) by A1, A2, A3, A4, A5, A6, Th20, NAT_1:25;
per cases ( i1 = i2 or i1 = i2 + 1 or i1 + 1 = i2 ) by A10, Th2, SEQM_3:41;
case i1 = i2 ; :: thesis: LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))
hence LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) by A7; :: thesis: verum
end;
case i1 = i2 + 1 ; :: thesis: (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))}
hence (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} by A2, A3, A4, A7, A9, Th14; :: thesis: verum
end;
case i1 + 1 = i2 ; :: thesis: (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))}
hence (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} by A1, A3, A5, A7, A8, Th14; :: thesis: verum
end;
end;