:: deftheorem deford defines ordered REALALG1:def 17 :
for R being Ring holds
( R is ordered iff ex P being Subset of R st P is positive_cone );