theorem :: REALALG1:38

for O being Ordering of F_Rat holds O = Positives(F_Rat)