theorem :: REALALG1:36

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