theorem Th20: :: GOBRD11:20

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