theorem Th5: :: GOBOARD5:5

for i, j being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }