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