:: deftheorem defppp defines -ordered REALALG2:def 7 :
for R being preordered Ring
for P being Preordering of R
for a being Element of R holds
( a is P -ordered iff a in P \/ (- P) );