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;
A10: 1 <= i + 1 by NAT_1:11;
A11: 1 <= j + 1 by NAT_1:11;
consider k, l being Element of NAT such that
A12: p = G * k,l and
A13: [k,l] in Indices G by A5, A7;
A14: ( 1 <= k & k <= len G & 1 <= l & l <= width G ) by A13, MATRIX_1:39;

A15: now

assume A16: ( k <> i & k <> i + 1 ) ; :: thesis: contradiction

per cases ( k < i or i + 1 < k ) by A16, NAT_1:9;

suppose k < i ; :: thesis: contradiction

then (G * k,l) `1 < (G * i,l) `1 by A8, A14, GOBOARD5:4;
then (G * k,l) `1 < (G * i,1) `1 by A1, A8, A14, 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, A12, Th19; :: thesis: verum

end;

suppose i + 1 < k ; :: thesis: contradiction

then (G * (i + 1),l) `1 < (G * k,l) `1 by A10, A14, GOBOARD5:4;
then (G * (i + 1),1) `1 < (G * k,l) `1 by A2, A10, A14, GOBOARD5:3;
then (G * (i + 1),j) `1 < (G * k,l) `1 by A2, A3, A9, A10, GOBOARD5:3;
hence contradiction by A1, A2, A3, A4, A6, A12, Th19; :: thesis: verum

end;

end;

end;

now

assume A17: ( l <> j & l <> j + 1 ) ; :: thesis: contradiction

per cases ( l < j or j + 1 < l ) by A17, NAT_1:9;

suppose l < j ; :: thesis: contradiction

then (G * k,l) `2 < (G * k,j) `2 by A9, A14, GOBOARD5:5;
then (G * k,l) `2 < (G * 1,j) `2 by A3, A9, A14, 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, A12, Th19; :: thesis: verum

end;

suppose j + 1 < l ; :: thesis: contradiction

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