:: deftheorem Def8 defines DecoratedTree-like TREES_2:def 8 :
for IT being Relation holds
( IT is DecoratedTree-like iff dom IT is Tree );