theorem Th23: :: GOBRD11:23

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