let G be Go-board; :: thesis: for i1, j1, i2, j2 being Element of NAT st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( j1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
( j1 + 1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} )
let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( j1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) implies ( j1 + 1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} ) )
assume that
A1: ( 1 <= i1 & i1 <= len G ) and
A2: ( 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G ) and
A3: ( 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) ) ; :: thesis: ( ( j1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) or ( j1 + 1 = j2 & (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} ) )
per cases ( j1 = j2 or j1 + 1 = j2 ) by A1, A2, A3, Th23;
case A4: j1 = j2 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)}
now
per cases ( i1 = i2 or i1 = i2 + 1 ) by A1, A2, A3, Th23;
suppose i1 = i2 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)}
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} by A2, A4, Th19; :: thesis: verum
end;
suppose i1 = i2 + 1 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)}
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} by A2, A4, Th20; :: thesis: verum
end;
end;
end;
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ; :: thesis: verum
end;
case A5: j1 + 1 = j2 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))}
now
per cases ( i1 = i2 or i1 = i2 + 1 ) by A1, A2, A3, Th23;
suppose i1 = i2 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))}
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} by A2, A5, Th17; :: thesis: verum
end;
suppose i1 = i2 + 1 ; :: thesis: (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))}
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} by A2, A5, Th18; :: thesis: verum
end;
end;
end;
hence (LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} ; :: thesis: verum
end;
end;