theorem :: REALALG1:39

Positives(INT.Ring) is Ordering of INT.Ring ;