let G be V9() Y_equal-in-column Y_increasing-in-line Matrix of ; :: thesis: width G = card (proj2 .: (Values G))
( width G <= card (proj2 .: (Values G)) & card (proj2 .: (Values G)) <= width G ) by Th23, Th24;
hence width G = card (proj2 .: (Values G)) by XXREAL_0:1; :: thesis: verum