theorem :: MATRIX10:54

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