:: deftheorem defines < REALALG2:def 6 :
for R being preordered Ring
for P being Preordering of R
for a, b being Element of R holds
( a < P,b iff ( a <= P,b & a <> b ) );