:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :
for IT being Function holds
( IT is FinTree-yielding iff rng IT is constituted-FinTrees );