:: deftheorem defines Subtree TREES_1:def 8 :
for T, b₂ being Tree holds
( b₂ is Subtree of T iff ex p being Element of T st b₂ = T | p );