let i1, i2, j1, j2 be Nat; :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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;

(G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1

let G1, G2 be Go-board; :: thesis: ( 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) ; :: thesis: (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;

A17: now :: thesis: not i2 <= i

assume A18:
(G2 * ((i2 -' 1),j2)) `1 < (G1 * ((i1 -' 1),j1)) `1
; :: thesis: contradictionassume
i2 <= i
; :: thesis: contradiction

then ( i = i2 or i2 < i ) by XXREAL_0:1;

hence contradiction by A4, A6, A13, A16, GOBOARD5:3; :: thesis: verum

end;then ( i = i2 or i2 < i ) by XXREAL_0:1;

hence contradiction by A4, A6, A13, A16, GOBOARD5:3; :: thesis: verum

now :: thesis: not i <= i2 -' 1

hence
contradiction
by A17, NAT_D:49; :: thesis: verumassume
i <= i2 -' 1
; :: thesis: contradiction

then ( i2 -' 1 = i or i < i2 -' 1 ) by XXREAL_0:1;

hence contradiction by A6, A18, A10, A12, A14, A9, GOBOARD5:3; :: thesis: verum

end;then ( i2 -' 1 = i or i < i2 -' 1 ) by XXREAL_0:1;

hence contradiction by A6, A18, A10, A12, A14, A9, GOBOARD5:3; :: thesis: verum