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