:: deftheorem Def15 defines tree TREES_3:def 15 :
for p being FinSequence st p is Tree-yielding holds
for b₂ being Tree holds
( b₂ = tree p iff for x being object holds
( x in b₂ iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) );