:: deftheorem defines MP-conectives MODAL_1:def 4 :
MP-conectives = [:{0,1,2},NAT:];