let G be V3() X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: len G <= card (proj1 .: (Values G))
0 <> width G by MATRIX_0:def 10;
then 1 <= width G by NAT_1:14;
then A1: 1 in Seg (width G) by FINSEQ_1:1;
then reconsider L = X_axis (Col (G,1)) as increasing FinSequence of REAL by GOBOARD1:def 7;
A2: card (rng L) = len L by FINSEQ_4:62
.= len (Col (G,1)) by GOBOARD1:def 1
.= len G by MATRIX_0:def 8 ;
A3: rng L = rng (proj1 * (Col (G,1))) by Th10
.= proj1 .: (rng (Col (G,1))) by RELAT_1:127 ;
rng (Col (G,1)) c= Values G by A1, Th12;
hence len G <= card (proj1 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; :: thesis: verum