consider x1, x2 being set such that
A1: x1 in {3} and
A2: ( x2 in NAT & p = [x1,x2] ) by ZFMISC_1:def 2;
x1 = 3 by A1, TARSKI:def 1;
hence (elementary_tree 0 ) --> p is MP-wff by A2, Th35; :: thesis: verum