theorem :: MODAL_1:41

for A being Element of MP-WFF holds
( A = VERUM or A is atomic MP-wff or A is negative MP-wff or A is necessitive MP-wff or A is conjunctive MP-wff )