let G be V21() Y_increasing-in-line Matrix of (TOP-REAL 2); :: thesis: width G <= card (proj2 .: (Values G))
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by NAT_1:14;
then A1: 1 in dom G by FINSEQ_3:27;
then reconsider L = Y_axis (Line G,1) as increasing FinSequence of REAL by GOBOARD1:def 8;
A2: card (rng L) = len L by FINSEQ_4:77
.= len (Line G,1) by GOBOARD1:def 4
.= width G by MATRIX_1:def 8 ;
A3: rng L = rng (proj2 * (Line G,1)) by Th17
.= proj2 .: (rng (Line G,1)) by RELAT_1:160 ;
rng (Line G,1) c= Values G by A1, Th19;
hence width G <= card (proj2 .: (Values G)) by A3, A2, NAT_1:44, RELAT_1:156; :: thesis: verum