theorem :: MATRIX10:46

for n being Nat
for M1, M2, M3, M4 being Matrix of n,REAL st M1 is_less_than M2 & M3 is_less_than M4 holds
M1 + M3 is_less_than M2 + M4