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 `2 = (G * (m,n)) `2 & not j = n holds
j = n -' 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 `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 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 `2 = (G * (m,n)) `2 ; :: thesis: ( j = n or j = n -' 1 )
A11: (G * (1,n)) `2 = (G * (m,n)) `2 by A5, A6, A7, A8, GOBOARD5:1;
A12: 1 <= len G by A1, A2, XXREAL_0:2;
per cases ( j = width G or j < width G ) by A4, XXREAL_0:1;
suppose j = width G ; :: thesis: ( j = n or j = n -' 1 )
hence ( j = n or j = n -' 1 ) by A1, A2, A5, A6, A7, A8, A9, A10, Th23; :: 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, A3, GOBRD11:32;
then consider r, s being Real such that
A13: p = |[r,s]| and
(G * (i,1)) `1 <= r and
r <= (G * ((i + 1),1)) `1 and
A14: (G * (1,j)) `2 <= s and
A15: s <= (G * (1,(j + 1))) `2 by A9;
A16: p `2 = s by A13, EUCLID:52;
( j <= n & n <= j + 1 )
proof
assume A17: ( not j <= n or not n <= j + 1 ) ; :: thesis: contradiction
end;
hence ( j = n or j = n -' 1 ) by Lm2; :: thesis: verum
end;
end;