theorem :: REALALG1:30

for R being preordered Ring
for P being Preordering of R holds OrdRel P is OrderRelation of R ;