theorem Th16: :: JORDAN1H:16

for G being empty-yielding X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G))