:: deftheorem defines Positives(F_Real) REALALG1:def 21 :
Positives(F_Real) = { r where r is Element of REAL : 0 <= r } ;