:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :
for IT being Function holds
( IT is Tree-yielding iff rng IT is constituted-Trees );