:: deftheorem Def16 defines atomic MODAL_1:def 16 :
for IT being MP-wff holds
( IT is atomic iff ex p being MP-variable st IT = @ p );