theorem :: ARYTM_2:20

( {} in REAL+ & one in REAL+ ) by Th1;