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*>)} )

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

hence
( not t in Leaves (elementary_tree 0) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
by TREES_1:def 5; :: thesis: verumnot 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;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