:: deftheorem defines <%> AFINSQ_1:def 2 :
for D being set holds <%> D = {} ;