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 for b₁ being Matrix of REAL st b₁ = 1,1 --> (- 1) holds
b₁ is Negative by Def2; :: thesis: verum