:: deftheorem defines the_arity_of MODAL_1:def 6 :
for a being Element of MP-conectives holds the_arity_of a = a `1 ;