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