let G be V3() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: len G = card (proj1 .: (Values G))
( len G <= card (proj1 .: (Values G)) & card (proj1 .: (Values G)) <= len G ) by Th14, Th15;
hence len G = card (proj1 .: (Values G)) by XXREAL_0:1; :: thesis: verum