set T = elementary_tree 0;
let t be Element of elementary_tree 0; :: according to BINTREE1:def 2 :: thesis: ( not t in Leaves (elementary_tree 0) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

now :: thesis: for s being FinSequence of NAT st s in elementary_tree 0 holds
not t is_a_proper_prefix_of s

let s be FinSequence of NAT ; :: thesis: ( s in elementary_tree 0 implies not t is_a_proper_prefix_of s )
assume s in elementary_tree 0 ; :: thesis: not t is_a_proper_prefix_of s
then s = {} by TARSKI:def 1, TREES_1:29;
hence not t is_a_proper_prefix_of s by TARSKI:def 1, TREES_1:29; :: thesis: verum

end;

hence ( not t in Leaves (elementary_tree 0) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) by TREES_1:def 5; :: thesis: verum