for R being preordered domRing
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