theorem c4: :: REALALG2:46

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