let i1, i2, j1, j2 be Nat; for G1, G2 being Go-board st G1 * ((i1 -' 1),j1) in Values G2 & 1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds
(G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1
let G1, G2 be Go-board; ( G1 * ((i1 -' 1),j1) in Values G2 & 1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) implies (G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1 )
assume that
A1:
G1 * ((i1 -' 1),j1) in Values G2
and
A2:
1 < i1
and
A3:
( i1 <= len G1 & 1 <= j1 & j1 <= width G1 )
and
A4:
1 < i2
and
A5:
i2 <= len G2
and
A6:
( 1 <= j2 & j2 <= width G2 )
and
A7:
G1 * (i1,j1) = G2 * (i2,j2)
; (G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1
set p = G1 * ((i1 -' 1),j1);
A8:
G1 * ((i1 -' 1),j1) in { (G2 * (i,j)) where i, j is Nat : [i,j] in Indices G2 }
by A1, MATRIX_0:39;
1 <= i2 -' 1
by A4, NAT_D:49;
then
i2 -' 1 < i2
by NAT_D:51;
then A9:
i2 -' 1 < len G2
by A5, XXREAL_0:2;
consider i, j being Nat such that
A10:
G1 * ((i1 -' 1),j1) = G2 * (i,j)
and
A11:
[i,j] in Indices G2
by A8;
A12:
1 <= i
by A11, MATRIX_0:32;
A13:
i <= len G2
by A11, MATRIX_0:32;
( 1 <= j & j <= width G2 )
by A11, MATRIX_0:32;
then A14: (G2 * (i,j)) `1 =
(G2 * (i,1)) `1
by A12, A13, GOBOARD5:2
.=
(G2 * (i,j2)) `1
by A6, A12, A13, GOBOARD5:2
;
A15:
1 <= i1 -' 1
by A2, NAT_D:49;
then
i1 -' 1 < i1
by NAT_D:51;
then A16:
(G2 * (i,j2)) `1 < (G2 * (i2,j2)) `1
by A3, A7, A15, A10, A14, GOBOARD5:3;
assume A18:
(G2 * ((i2 -' 1),j2)) `1 < (G1 * ((i1 -' 1),j1)) `1
; contradiction
hence
contradiction
by A17, NAT_D:49; verum