:: deftheorem Def3 defines Nonpositive MATRIX10:def 3 :
for M being Matrix of REAL holds
( M is Nonpositive iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 );