:: deftheorem defines <= REALALG1:def 18 :
for R being preordered Ring
for P being Preordering of R
for a, b being Element of R holds
( a <= P,b iff b - a in P );