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