:: deftheorem defines Subtrees TREES_9:def 7 :
for t being DecoratedTree holds Subtrees t = { (t | p) where p is Node of t : verum } ;