:: deftheorem defpord defines preordered REALALG1:def 16 :
for R being Ring holds
( R is preordered iff ex P being Subset of R st P is prepositive_cone );