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

hereby :: thesis: ( 0 < len M & 0 < width M implies not M is empty-yielding )

assume not M is empty-yielding ; :: thesis: ( 0 < len M & 0 < width M )
then ( 0 <> len M & 0 <> width M ) by Def5;
hence ( 0 < len M & 0 < width M ) ; :: thesis: verum

end;

assume ( 0 < len M & 0 < width M ) ; :: thesis: not M is empty-yielding
hence not M is empty-yielding by Def5; :: thesis: verum