:: deftheorem defines Positives(INT.Ring) REALALG1:def 23 :
Positives(INT.Ring) = { i where i is Element of INT : 0 <= i } ;