:: deftheorem defines rsgn COMPLEX3:def 5 :
for a being Complex holds rsgn a = Re (director a);