:: deftheorem defines Attrs ABCMIZ_1:def 19 :
Attrs = [:{an_Adj},[:QuasiLoci,NAT:]:];