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