for G being V3() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G))