theorem :: REALALG2:21

for P being Preordering of F_Rat holds P = Positives(F_Rat) by REALALG1:38;