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

hereby :: thesis: ( 0 < len M & 0 < width M implies not M is V3() )

assume M is V3() ; :: thesis: ( 0 < len M & 0 < width M )
then ( 0 <> len M & 0 <> width M ) by Def3;
hence ( 0 < len M & 0 < width M ) ; :: thesis: verum

end;

assume ( 0 < len M & 0 < width M ) ; :: thesis: M is V3()
hence M is V3() by Def3; :: thesis: verum