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