theorem :: REALALG2:20

for P being Preordering of INT.Ring holds P = Positives(INT.Ring) by REALALG1:40;