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:13, TREES_1:29;
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 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] ) ) by A2, A3, CARD_1:27, FUNCOP_1:7, TREES_2:def 12; :: thesis: verum
end;
hence (elementary_tree 0) --> [0,0] is MP-wff by Def5; :: thesis: verum