theorem Th17: :: JORDAN1H:17

for G being empty-yielding Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G))