theorem c5: :: REALALG2:47

for R being preordered Ring
for P being Preordering of R
for a, b, c being Element of R st a <= P,b & 0. R <= P,c holds
a * c <= P,b * c