let G be V3() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2); :: thesis: width G = card (proj2 .: (Values G))
( width G <= card (proj2 .: (Values G)) & card (proj2 .: (Values G)) <= width G ) by Th17, Th18;
hence width G = card (proj2 .: (Values G)) by XXREAL_0:1; :: thesis: verum