theorem :: MATRIX_0:44

for D being non empty set
for M being Matrix of D holds
( M is empty-yielding iff ( 0 < len M & 0 < width M ) ) ;