for i, j being Nat st [i,j] in Indices (1,1 --> (- 1)) holds
(1,1 --> (- 1)) * i,j < 0

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1,1 --> (- 1)) implies (1,1 --> (- 1)) * i,j < 0 )
assume [i,j] in Indices (1,1 --> (- 1)) ; :: thesis: (1,1 --> (- 1)) * i,j < 0
then (1,1 --> (- 1)) * i,j = - 1 by MATRIX_2:1;
hence (1,1 --> (- 1)) * i,j < 0 ; :: thesis: verum

end;

hence 1,1 --> (- 1) is Negative Matrix of REAL by Def2; :: thesis: verum