:: deftheorem defines ** MEMBER_1:def 20 :
for A being complex-membered set
for a being Complex holds a ** A = {a} ** A;