let i, j be Nat; :: thesis: for G being Go-board
for p being Point of (TOP-REAL 2) st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) & not p = G * (i,j) & not p = G * (i,(j + 1)) & not p = G * ((i + 1),(j + 1)) holds
p = G * ((i + 1),j)
let G be Go-board; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) & not p = G * (i,j) & not p = G * (i,(j + 1)) & not p = G * ((i + 1),(j + 1)) holds
p = G * ((i + 1),j)
let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) & not p = G * (i,j) & not p = G * (i,(j + 1)) & not p = G * ((i + 1),(j + 1)) implies p = G * ((i + 1),j) )
assume that
A1: 1 <= i and
A2: i + 1 <= len G and
A3: 1 <= j and
A4: j + 1 <= width G and
A5: p in Values G and
A6: p in cell (G,i,j) ; :: thesis: ( p = G * (i,j) or p = G * (i,(j + 1)) or p = G * ((i + 1),(j + 1)) or p = G * ((i + 1),j) )
A7: Values G = { (G * (k,l)) where k, l is Nat : [k,l] in Indices G } by MATRIX_0:39;
A8: i < len G by A2, NAT_1:13;
A9: j < width G by A4, NAT_1:13;
consider k, l being Nat such that
A10: p = G * (k,l) and
A11: [k,l] in Indices G by A5, A7;
A12: 1 <= k by A11, MATRIX_0:32;
A13: l <= width G by A11, MATRIX_0:32;
A14: 1 <= l by A11, MATRIX_0:32;
A15: k <= len G by A11, MATRIX_0:32;
A16: 1 <= j + 1 by NAT_1:11;
A17: now :: thesis: ( l <> j implies not l <> j + 1 )
assume A18: ( l <> j & l <> j + 1 ) ; :: thesis: contradiction
per cases ( l < j or j + 1 < l ) by A18, NAT_1:9;
suppose l < j ; :: thesis: contradiction
then (G * (k,l)) `2 < (G * (k,j)) `2 by A9, A12, A15, A14, GOBOARD5:4;
then (G * (k,l)) `2 < (G * (1,j)) `2 by A3, A9, A12, A15, GOBOARD5:1;
then (G * (k,l)) `2 < (G * (i,j)) `2 by A1, A3, A8, A9, GOBOARD5:1;
hence contradiction by A1, A2, A3, A4, A6, A10, Th17; :: thesis: verum
end;
suppose j + 1 < l ; :: thesis: contradiction
then (G * (k,(j + 1))) `2 < (G * (k,l)) `2 by A16, A12, A15, A13, GOBOARD5:4;
then (G * (1,(j + 1))) `2 < (G * (k,l)) `2 by A4, A16, A12, A15, GOBOARD5:1;
then (G * (i,(j + 1))) `2 < (G * (k,l)) `2 by A1, A4, A8, A16, GOBOARD5:1;
hence contradiction by A1, A2, A3, A4, A6, A10, Th17; :: thesis: verum
end;
end;
end;
A19: 1 <= i + 1 by NAT_1:11;
now :: thesis: ( k <> i implies not k <> i + 1 )
assume A20: ( k <> i & k <> i + 1 ) ; :: thesis: contradiction
per cases ( k < i or i + 1 < k ) by A20, NAT_1:9;
suppose k < i ; :: thesis: contradiction
then (G * (k,l)) `1 < (G * (i,l)) `1 by A8, A12, A14, A13, GOBOARD5:3;
then (G * (k,l)) `1 < (G * (i,1)) `1 by A1, A8, A14, A13, GOBOARD5:2;
then (G * (k,l)) `1 < (G * (i,j)) `1 by A1, A3, A8, A9, GOBOARD5:2;
hence contradiction by A1, A2, A3, A4, A6, A10, Th17; :: thesis: verum
end;
suppose i + 1 < k ; :: thesis: contradiction
then (G * ((i + 1),l)) `1 < (G * (k,l)) `1 by A19, A15, A14, A13, GOBOARD5:3;
then (G * ((i + 1),1)) `1 < (G * (k,l)) `1 by A2, A19, A14, A13, GOBOARD5:2;
then (G * ((i + 1),j)) `1 < (G * (k,l)) `1 by A2, A3, A9, A19, GOBOARD5:2;
hence contradiction by A1, A2, A3, A4, A6, A10, Th17; :: thesis: verum
end;
end;
end;
hence ( p = G * (i,j) or p = G * (i,(j + 1)) or p = G * ((i + 1),(j + 1)) or p = G * ((i + 1),j) ) by A10, A17; :: thesis: verum