theorem Th8: :: GOBOARD5:8

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