let D be non empty set ; :: thesis: for M being empty-yielding Matrix of D holds
( 1 <= len M & 1 <= width M )
let M be empty-yielding Matrix of D; :: thesis: ( 1 <= len M & 1 <= width M )
( not len M = 0 & not width M = 0 ) by MATRIX_0:def 10;
hence ( 1 <= len M & 1 <= width M ) by NAT_1:14; :: thesis: verum