let G be empty-yielding Y_increasing-in-line Matrix of (TOP-REAL 2); :: thesis: width G <= card (proj2 .: (Values G))
0 <> len G by MATRIX_0:def 10;
then 1 <= len G by NAT_1:14;
then A1: 1 in dom G by FINSEQ_3:25;
then reconsider L = Y_axis (Line (G,1)) as increasing FinSequence of REAL by GOBOARD1:def 6;
A2: card (rng L) = len L by FINSEQ_4:62
.= len (Line (G,1)) by GOBOARD1:def 2
.= width G by MATRIX_0:def 7 ;
A3: rng L = rng (proj2 * (Line (G,1))) by Th11
.= proj2 .: (rng (Line (G,1))) by RELAT_1:127 ;
rng (Line (G,1)) c= Values G by A1, Th13;
hence width G <= card (proj2 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; :: thesis: verum