:: deftheorem defines DTree-yielding TREES_3:def 11 :
for IT being Function holds
( IT is DTree-yielding iff rng IT is constituted-DTrees );