:: deftheorem defines /\ REALALG2:def 2 :
for R being ordered Ring
for P being Preordering of R holds /\ (P,R) = { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } ;