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

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:56;
hence not t is_a_proper_prefix_of s by TARSKI:def 1, TREES_1:56; :: thesis: verum

end;

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