:: deftheorem defines R^1 TOPREALB:def 3 :
for A being Subset of REAL holds R^1 A = A;