theorem Th18: :: JORDAN1H:18

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