:: deftheorem Def6 defines | TREES_1:def 6 :
for T being Tree
for p being FinSequence of NAT st p in T holds
for b₃ being Tree holds
( b₃ = T | p iff for q being FinSequence of NAT holds
( q in b₃ iff p ^ q in T ) );