:: deftheorem defines root TREES_9:def 1 :
for IT being DecoratedTree holds
( IT is root iff dom IT = elementary_tree 0 );