theorem Th25: :: MODAL_1:30

for n being Nat holds (elementary_tree 0) --> [3,n] is MP-wff