theorem Th15: :: JORDAN1H:15

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