:: deftheorem defines -- MEMBER_1:def 8 :
for A, B being complex-membered set holds A -- B = A ++ (-- B);