theorem :: REALALG1:40

for O being Ordering of INT.Ring holds O = Positives(INT.Ring)