:: deftheorem defines zero3 MOD_2:def 19 :
zero3 = 0 ;