:: deftheorem defines '&' MODAL_1:def 10 :
for A, B being MP-wff holds A '&' B = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);