:: deftheorem defines Leaves TREES_2:def 9 :
for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T));