consider x1, x2 being object 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, Th25; :: thesis: verum