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