:: deftheorem defines R^1 TOPREALB:def 2 :
for r being Real holds R^1 r = r;