let n be Nat; :: thesis: for M1 being Matrix of n, REAL st M1 is Positive holds
M1 is Nonnegative
let M1 be Matrix of n, REAL ; :: thesis: ( M1 is Positive implies M1 is Nonnegative )
assume M1 is Positive ; :: thesis: M1 is Nonnegative
then for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j >= 0 by Def1;
hence M1 is Nonnegative by Def4; :: thesis: verum