let G be Go-board; :: thesis: for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,i,j & p `2 = (G * m,n) `2 & not j = n holds
j = n -' 1
let i, j, m, n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,i,j & p `2 = (G * m,n) `2 & not j = n holds
j = n -' 1
let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1 <= n & n <= width G & p in cell G,i,j & p `2 = (G * m,n) `2 & not j = n implies j = n -' 1 )
assume that
A1: ( 1 <= i & i < len G ) and
A2: ( 1 <= j & j <= width G ) and
A3: ( 1 <= m & m <= len G ) and
A4: ( 1 <= n & n <= width G ) and
A5: p in cell G,i,j and
A6: p `2 = (G * m,n) `2 ; :: thesis: ( j = n or j = n -' 1 )
A7: 1 <= len G by A1, XXREAL_0:2;
A8: (G * 1,n) `2 = (G * m,n) `2 by A3, A4, GOBOARD5:2;

per cases ( j = width G or j < width G ) by A2, XXREAL_0:1;

suppose j = width G ; :: thesis: ( j = n or j = n -' 1 )

hence ( j = n or j = n -' 1 ) by A1, A3, A4, A5, A6, Th24; :: thesis: verum

end;

suppose j < width G ; :: thesis: ( j = n or j = n -' 1 )

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 A1, A2, GOBRD11:32;
then consider r, s being Real such that
A9: p = |[r,s]| and
( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) and
A10: ( (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) by A5;
A11: p `2 = s by A9, EUCLID:56;
( j <= n & n <= j + 1 )

proof

assume A12: ( not j <= n or not n <= j + 1 ) ; :: thesis: contradiction

per cases ( j > n or n > j + 1 ) by A12;

suppose j > n ; :: thesis: contradiction

hence contradiction by A2, A4, A6, A7, A8, A10, A11, GOBOARD5:5; :: thesis: verum

end;

suppose A13: n > j + 1 ; :: thesis: contradiction

1 <= j + 1 by NAT_1:11;
hence contradiction by A4, A6, A7, A8, A10, A11, A13, GOBOARD5:5; :: thesis: verum

end;

end;

end;

hence ( j = n or j = n -' 1 ) by Lm2; :: thesis: verum

end;

end;