let i, j, k be 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;
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:4;
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;
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:52;
p `1 = r9 by A9, EUCLID:52;
then (G * (k,1)) `1 <= (G * (1,1)) `1 by A10, A13, A15, A17, XXREAL_0:2;
hence contradiction by A5, A11, A16, GOBOARD5:3; :: 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:6;
A23: p `1 = r by A19, EUCLID:52;
p `1 = r9 by A9, EUCLID:52;
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:3; :: thesis: verum

end;

end;