REAL+ = { r where r is Real : 0 <= r }