:: deftheorem defines * ABCMIZ_1:def 7 :
* = 0 ;