theorem Th19: :: JORDAN1H:19

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