:: deftheorem defines is_less_or_equal_with MATRIX10:def 6 :
for M1, M2 being Matrix of REAL holds
( M1 is_less_or_equal_with M2 iff for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j) );