:: deftheorem defines Leaf TREES_1:def 7 :
for T being Tree st Leaves T <> {} holds
for b₂ being Element of T holds
( b₂ is Leaf of T iff b₂ in Leaves T );