:: deftheorem defines /// MEMBER_1:def 12 :
for A, B being complex-membered set holds A /// B = A ** (B "");