let G be Go-board; :: thesis: for i, j, m, n being 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 `1 = (G * (m,n)) `1 & not i = m holds

i = m -' 1

let i, j, m, n be 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 `1 = (G * (m,n)) `1 & not i = m holds

i = m -' 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 `1 = (G * (m,n)) `1 & not i = m implies i = m -' 1 )

assume that

A1: 1 <= i and

A2: i <= len G and

A3: 1 <= j and

A4: j < width G and

A5: 1 <= m and

A6: m <= len G and

A7: 1 <= n and

A8: n <= width G and

A9: p in cell (G,i,j) and

A10: p `1 = (G * (m,n)) `1 ; :: thesis: ( i = m or i = m -' 1 )

A11: (G * (m,1)) `1 = (G * (m,n)) `1 by A5, A6, A7, A8, GOBOARD5:2;

A12: 1 <= width G by A3, A4, XXREAL_0:2;

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 `1 = (G * (m,n)) `1 & not i = m holds

i = m -' 1

let i, j, m, n be 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 `1 = (G * (m,n)) `1 & not i = m holds

i = m -' 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 `1 = (G * (m,n)) `1 & not i = m implies i = m -' 1 )

assume that

A1: 1 <= i and

A2: i <= len G and

A3: 1 <= j and

A4: j < width G and

A5: 1 <= m and

A6: m <= len G and

A7: 1 <= n and

A8: n <= width G and

A9: p in cell (G,i,j) and

A10: p `1 = (G * (m,n)) `1 ; :: thesis: ( i = m or i = m -' 1 )

A11: (G * (m,1)) `1 = (G * (m,n)) `1 by A5, A6, A7, A8, GOBOARD5:2;

A12: 1 <= width G by A3, A4, XXREAL_0:2;

per cases
( i = len G or i < len G )
by A2, XXREAL_0:1;

end;

suppose
i < len G
; :: thesis: ( i = m or i = m -' 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, A3, A4, GOBRD11:32;

then consider r, s being Real such that

A13: p = |[r,s]| and

A14: (G * (i,1)) `1 <= r and

A15: r <= (G * ((i + 1),1)) `1 and

(G * (1,j)) `2 <= s and

s <= (G * (1,(j + 1))) `2 by A9;

A16: p `1 = r by A13, EUCLID:52;

( i <= m & m <= i + 1 )

end;then consider r, s being Real such that

A13: p = |[r,s]| and

A14: (G * (i,1)) `1 <= r and

A15: r <= (G * ((i + 1),1)) `1 and

(G * (1,j)) `2 <= s and

s <= (G * (1,(j + 1))) `2 by A9;

A16: p `1 = r by A13, EUCLID:52;

( i <= m & m <= i + 1 )

proof

hence
( i = m or i = m -' 1 )
by Lm2; :: thesis: verum
assume A17:
( not i <= m or not m <= i + 1 )
; :: thesis: contradiction

end;