for n being Nat
for M1 being Matrix of n,REAL st M1 is Positive holds
M1 is Nonnegative ;