theorem :: REALALG1:35

Positives(F_Real) is Ordering of F_Real ;