:: deftheorem defines OrdRel REALALG1:def 19 :
for R being preordered Ring
for P being Preordering of R holds OrdRel P = { [a,b] where a, b is Element of R : a <= P,b } ;