:: deftheorem defines RNS_Real DUALSP02:def 3 :
RNS_Real = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);