theorem Th21: :: GOBRD11:21

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