theorem Th23: :: MODAL_1:28

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