let i, j be Element of 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 Element of NAT : [k,l] in Indices G } by GOBRD13:7;
A8: i < len G by A2, NAT_1:13;
A9: j < width G by A4, NAT_1:13;
consider k, l being Element of NAT such that
A10: p = G * k,l and
A11: [k,l] in Indices G by A5, A7;
A12: 1 <= k by A11, MATRIX_1:39;
A13: l <= width G by A11, MATRIX_1:39;
A14: 1 <= l by A11, MATRIX_1:39;
A15: k <= len G by A11, MATRIX_1:39;
A16: 1 <= j + 1 by NAT_1:11;

A17: now

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:5;
then (G * k,l) `2 < (G * 1,j) `2 by A3, A9, A12, A15, GOBOARD5:2;
then (G * k,l) `2 < (G * i,j) `2 by A1, A3, A8, A9, GOBOARD5:2;
hence contradiction by A1, A2, A3, A4, A6, A10, Th19; :: 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:5;
then (G * 1,(j + 1)) `2 < (G * k,l) `2 by A4, A16, A12, A15, GOBOARD5:2;
then (G * i,(j + 1)) `2 < (G * k,l) `2 by A1, A4, A8, A16, GOBOARD5:2;
hence contradiction by A1, A2, A3, A4, A6, A10, Th19; :: thesis: verum

end;

end;

end;

A19: 1 <= i + 1 by NAT_1:11;

now

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:4;
then (G * k,l) `1 < (G * i,1) `1 by A1, A8, A14, A13, GOBOARD5:3;
then (G * k,l) `1 < (G * i,j) `1 by A1, A3, A8, A9, GOBOARD5:3;
hence contradiction by A1, A2, A3, A4, A6, A10, Th19; :: 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:4;
then (G * (i + 1),1) `1 < (G * k,l) `1 by A2, A19, A14, A13, GOBOARD5:3;
then (G * (i + 1),j) `1 < (G * k,l) `1 by A2, A3, A9, A19, GOBOARD5:3;
hence contradiction by A1, A2, A3, A4, A6, A10, Th19; :: 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