theorem :: JORDAN9:25

for i, j, k being Nat
for G being Go-board st [i,j] in Indices G & 1 <= k & k <= len G holds
(G * (i,j)) `2 <= (G * (k,(width G))) `2