let n be Nat; :: thesis: (elementary_tree 0) --> [3,n] is MP-wff
( 3 in NAT & n in NAT ) by ORDINAL1:def 12;
then reconsider 3n = [3,n] as Element of [:NAT,NAT:] by ZFMISC_1:87;
set x = (elementary_tree 0) --> 3n;
A1: dom ((elementary_tree 0) --> 3n) = {{}} by FUNCOP_1:13, TREES_1:29;
reconsider x = (elementary_tree 0) --> 3n as finite DecoratedTree of [:NAT,NAT:] ;
A2: dom x = elementary_tree 0 by FUNCOP_1:13;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 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

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

end;

hence branchdeg v <= 2 by CARD_1:27, TREES_2:def 12; :: thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 m being Nat st x . v = [3,m] ) by A2, FUNCOP_1:7; :: thesis: ( ( 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 = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A3, CARD_1:27, TREES_2:def 12; :: thesis: verum

end;

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