:: deftheorem defines -- MEMBER_1:def 7 :
for F, G being ext-real-membered set holds F -- G = F ++ (-- G);