:: deftheorem defines <*> FINSEQ_1:def 6 :
for D being set holds <*> D = {} ;