theorem :: MATRIX10:15

for a being Real
for n being Nat
for M being Matrix of n,REAL st a < 0 & M is Negative holds
a * M is Positive