theorem :: REALALG2:62

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