for i, j being Nat st [i,j] in Indices ((1,1) --> 1) holds
((1,1) --> 1) * (i,j) > 0 by MATRIX_2:1;
hence for b₁ being Matrix of REAL st b₁ = (1,1) --> 1 holds
b₁ is Positive by Def1; :: thesis: verum