theorem :: REALALG2:58

for R being preordered domRing
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 by c5, GCD_1:1;