let i, k, j be Element of NAT ; :: thesis: for G being Go-board st i + k < len G & 1 <= j & j < width G & cell G,i,j meets cell G,(i + k),j holds
k <= 1
let G be Go-board; :: thesis: ( i + k < len G & 1 <= j & j < width G & cell G,i,j meets cell G,(i + k),j implies k <= 1 )
assume that
A1: i + k < len G and
A2: 1 <= j and
A3: j < width G and
A4: cell G,i,j meets cell G,(i + k),j and
A5: k > 1 ; :: thesis: contradiction
(cell G,i,j) /\ (cell G,(i + k),j) <> {} by A4, XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A6: p in (cell G,i,j) /\ (cell G,(i + k),j) by SUBSET_1:10;
A7: p in cell G,i,j by A6, XBOOLE_0:def 4;
A8: p in cell G,(i + k),j by A6, XBOOLE_0:def 4;
i + k >= 1 by A5, NAT_1:12;
then cell G,(i + k),j = { |[r9,s9]| where r9, s9 is Real : ( (G * (i + k),1) `1 <= r9 & r9 <= (G * ((i + k) + 1),1) `1 & (G * 1,j) `2 <= s9 & s9 <= (G * 1,(j + 1)) `2 ) } by A1, A2, A3, GOBRD11:32;
then consider r9, s9 being Real such that
A9: p = |[r9,s9]| and
A10: (G * (i + k),1) `1 <= r9 and
r9 <= (G * ((i + k) + 1),1) `1 and
(G * 1,j) `2 <= s9 and
s9 <= (G * 1,(j + 1)) `2 by A8;
A11: 1 < width G by A2, A3, XXREAL_0:2;
( i = 0 or i > 0 ) by NAT_1:3;
then A12: ( i = 0 or i >= 1 + 0 ) by NAT_1:9;

per cases ( i = 0 or i >= 1 ) by A12;

suppose A13: i = 0 ; :: thesis: contradiction

then cell G,i,j = { |[r,s]| where r, s is Real : ( r <= (G * 1,1) `1 & (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) } by A2, A3, GOBRD11:26;
then consider r, s being Real such that
A14: p = |[r,s]| and
A15: r <= (G * 1,1) `1 and
(G * 1,j) `2 <= s and
s <= (G * 1,(j + 1)) `2 by A7;
A16: k <= len G by A1, NAT_1:12;
A17: p `1 = r by A14, EUCLID:56;
p `1 = r9 by A9, EUCLID:56;
then (G * k,1) `1 <= (G * 1,1) `1 by A10, A13, A15, A17, XXREAL_0:2;
hence contradiction by A5, A11, A16, GOBOARD5:4; :: thesis: verum

end;

suppose A18: i >= 1 ; :: thesis: contradiction

i < len G by A1, NAT_1:12;
then cell G,i,j = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 & (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) } by A2, A3, A18, GOBRD11:32;
then consider r, s being Real such that
A19: p = |[r,s]| and
(G * i,1) `1 <= r and
A20: r <= (G * (i + 1),1) `1 and
(G * 1,j) `2 <= s and
s <= (G * 1,(j + 1)) `2 by A7;
A21: 1 <= i + 1 by NAT_1:12;
A22: i + 1 < k + i by A5, XREAL_1:8;
A23: p `1 = r by A19, EUCLID:56;
p `1 = r9 by A9, EUCLID:56;
then (G * (i + k),1) `1 <= (G * (i + 1),1) `1 by A10, A20, A23, XXREAL_0:2;
hence contradiction by A1, A11, A21, A22, GOBOARD5:4; :: thesis: verum

end;

end;