let G be empty-yielding Matrix of (TOP-REAL 2); :: thesis: ( 1 <= len G & 1 <= width G )
( not len G = 0 & not width G = 0 ) by MATRIX_0:def 10;
hence ( 1 <= len G & 1 <= width G ) by NAT_1:14; :: thesis: verum