let G be V9() X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: len G <= card (proj1 .: (Values G))
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by NAT_1:14;
then A1: 1 in Seg (width G) by FINSEQ_1:3;
then reconsider L = X_axis (Col G,1) as increasing FinSequence of REAL by GOBOARD1:def 9;
A2: card (rng L) = len L by FINSEQ_4:77
.= len (Col G,1) by GOBOARD1:def 3
.= len G by MATRIX_1:def 9 ;
A3: rng L = rng (proj1 * (Col G,1)) by Th16
.= proj1 .: (rng (Col G,1)) by RELAT_1:160 ;
rng (Col G,1) c= Values G by A1, Th18;
hence len G <= card (proj1 .: (Values G)) by A3, A2, NAT_1:44, RELAT_1:156; :: thesis: verum