theorem Th7: :: GOBOARD5:7

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,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }