:: deftheorem defines @ MODAL_1:def 14 :
for p being MP-variable holds @ p = (elementary_tree 0) --> p;