theorem :: REALALG2:65

for R being preordered Ring
for P being Preordering of R
for a being b₂ -ordered Element of R holds
( not a is P -positive iff a <= P, 0. R )