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