theorem :: REALALG2:63

for R being preordered Ring
for P being Preordering of R
for a being Element of R holds
( a is P -negative iff a < P, 0. R ) by x2;