theorem Th22: :: MODAL_1:27

for A being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff