theorem Th14: :: JORDAN1H:14

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