theorem Th17: :: JORDAN1H:17

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