theorem Th14: :: JORDAN1H:14

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