theorem Th18: :: GOBRD11:18

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