let i1, j1, i2, j2 be Element of NAT ; :: thesis: for G1, G2 being Go-board st G1 * i1,(j1 + 1) 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
(G2 * i2,(j2 + 1)) `2 <= (G1 * i1,(j1 + 1)) `2
let G1, G2 be Go-board; :: thesis: ( G1 * i1,(j1 + 1) 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 (G2 * i2,(j2 + 1)) `2 <= (G1 * i1,(j1 + 1)) `2 )
assume that
A1: G1 * i1,(j1 + 1) in Values G2 and
A2: ( 1 <= i1 & i1 <= len G1 & 1 <= j1 ) and
A3: j1 < width G1 and
A4: ( 1 <= i2 & i2 <= len G2 ) and
A5: 1 <= j2 and
A6: j2 < width G2 and
A7: G1 * i1,j1 = G2 * i2,j2 ; :: thesis: (G2 * i2,(j2 + 1)) `2 <= (G1 * i1,(j1 + 1)) `2
set p = G1 * i1,(j1 + 1);
G1 * i1,(j1 + 1) in { (G2 * i,j) where i, j is Element of NAT : [i,j] in Indices G2 } by A1, Th7;
then consider i, j being Element of NAT such that
A8: G1 * i1,(j1 + 1) = G2 * i,j and
A9: [i,j] in Indices G2 ;
A10: 1 <= j by A9, MATRIX_1:39;
A11: j <= width G2 by A9, MATRIX_1:39;
( 1 <= i & i <= len G2 ) by A9, MATRIX_1:39;
then A12: (G2 * i,j) `2 = (G2 * 1,j) `2 by A10, A11, GOBOARD5:2
.= (G2 * i2,j) `2 by A4, A10, A11, GOBOARD5:2 ;
( j1 < j1 + 1 & j1 + 1 <= width G1 ) by A3, NAT_1:13;
then A13: (G2 * i2,j2) `2 < (G2 * i2,j) `2 by A2, A7, A8, A12, GOBOARD5:5;

A14: now

assume j <= j2 ; :: thesis: contradiction
then ( j = j2 or j < j2 ) by XXREAL_0:1;
hence contradiction by A4, A6, A10, A13, GOBOARD5:5; :: thesis: verum

end;

assume A15: (G1 * i1,(j1 + 1)) `2 < (G2 * i2,(j2 + 1)) `2 ; :: thesis: contradiction
A16: 1 <= j2 + 1 by A5, NAT_1:13;

now

assume j2 + 1 <= j ; :: thesis: contradiction
then ( j2 + 1 = j or j2 + 1 < j ) by XXREAL_0:1;
hence contradiction by A4, A15, A8, A11, A12, A16, GOBOARD5:5; :: thesis: verum

end;

hence contradiction by A14, NAT_1:13; :: thesis: verum