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