:: deftheorem defines 1r COMPLEX1:def 4 :
1r = 1;