for i, j being Nat st [i,j] in Indices (n,n --> (- 1)) holds
(n,n --> (- 1)) * i,j <= 0 by MATRIX_2:1;
hence n,n --> (- 1) is Nonpositive Matrix of n, REAL by Def3; :: thesis: verum