theorem Th8: :: GOBRD13:15

for i1, i2, j1, j2 being Nat
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