let G be Go-board; 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; 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); ( 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
; ( 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;
suppose
i < len G
;
( 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 )
proof
assume A17:
( not
i <= m or not
m <= i + 1 )
;
contradiction
end; hence
(
i = m or
i = m -' 1 )
by Lm2;
verum end; end;