theorem Th6: :: GOBOARD5:6

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