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