:: deftheorem Def18 defines necessitive MODAL_1:def 18 :
for IT being MP-wff holds
( IT is necessitive iff ex A being MP-wff st IT = (#) A );