theorem ord2: :: REALALG1:24

for R being preordered Ring
for P being Preordering of R holds QS R c= P