let n be Nat; :: thesis: for M being Matrix of n, REAL st M is Negative holds
M is Nonpositive
let M be Matrix of n, REAL ; :: thesis: ( M is Negative implies M is Nonpositive )
assume M is Negative ; :: thesis: M is Nonpositive
then for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 by Def2;
hence M is Nonpositive by Def3; :: thesis: verum