theorem :: GOBOARD6:28
for j being Nat
for p being Point of (TOP-REAL 2)
for G being Go-board st j < width G & p in Int (h_strip (G,j)) holds
p `2 < (G * (1,(j + 1))) `2