set x = (elementary_tree 0 ) --> [0 ,0 ];
reconsider x = (elementary_tree 0 ) --> [0 ,0 ] as finite DecoratedTree of [:NAT ,NAT :] ;
A1: dom x = {{} } by FUNCOP_1:19, TREES_1:56;
A2: dom x = elementary_tree 0 by FUNCOP_1:19;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

proof

let v be Element of dom x; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
A3: succ v = {}

proof

consider y being Element of succ v;
assume not succ v = {} ; :: thesis: contradiction
then y in succ v ;
then y in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def 5;
then ex m being Element of NAT st
( y = v ^ <*m*> & v ^ <*m*> in dom x ) ;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

hence branchdeg v <= 2 by CARD_1:47, TREES_2:def 13; :: thesis: ( ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
thus ( ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) by A2, A3, CARD_1:47, FUNCOP_1:13, TREES_2:def 13; :: thesis: verum

end;

hence (elementary_tree 0 ) --> [0 ,0 ] is MP-wff by Def6; :: thesis: verum