theorem :: REAL_1:1

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