:: deftheorem defines /// MEMBER_1:def 11 :
for F, G being ext-real-membered set holds F /// G = F ** (G "");