theorem :: REALALG2:57

for R being preordered Ring
for P being Preordering of R
for a, b, c being Element of R st a < P,b holds
a + c < P,b + c by c4, RLVECT_1:8;