:: deftheorem defines ADTS TEX_1:def 3 :
for D being set holds ADTS D = TopStruct(# D,(cobool D) #);