:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :
for IT being set holds
( IT is constituted-DTrees iff for x being object st x in IT holds
x is DecoratedTree );