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