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