theorem :: MATRIX10:29
for a being Real
for n being Nat
for M being Matrix of n,REAL st a <= 0 & M is Positive holds
a * M is Nonpositive