:: deftheorem defines (#) MODAL_1:def 9 :
for A being MP-wff holds (#) A = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);