theorem Th9: :: GOBOARD5:9

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