:: deftheorem Def3 defines constituted-Trees TREES_3:def 3 :
for IT being set holds
( IT is constituted-Trees iff for x being object st x in IT holds
x is Tree );