:: deftheorem defines "" MEMBER_1:def 4 :
for A being complex-membered set holds A "" = { (c ") where c is Complex : c in A } ;