:: deftheorem Def5 defines Leaves TREES_1:def 5 :
for T being Tree
for b₂ being Subset of T holds
( b₂ = Leaves T iff for p being FinSequence of NAT holds
( p in b₂ iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) );