theorem Th22: :: GOBRD11:22

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