let n be Nat; :: thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 is_less_or_equal_with M2
let M1, M2 be Matrix of n, REAL ; :: thesis: ( M1 is_less_than M2 implies M1 is_less_or_equal_with M2 )
assume M1 is_less_than M2 ; :: thesis: M1 is_less_or_equal_with M2
then for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j) by Def5;
hence M1 is_less_or_equal_with M2 by Def6; :: thesis: verum