:: deftheorem Def3 defines finite-order TREES_9:def 3 :
for IT being DecoratedTree holds
( IT is finite-order iff dom IT is finite-order );