:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :
for IT being set holds
( IT is constituted-FinTrees iff for x being object st x in IT holds
x is finite Tree );