:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :
for T being finite Tree
for b₂ being Tree holds
( b₂ is T-Substitution of T iff for t being Element of b₂ holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) );