:: deftheorem Def7 defines Trees TREES_3:def 7 :
for D being non empty set
for b₂ being DTree-set of D holds
( b₂ = Trees D iff for T being DecoratedTree of D holds T in b₂ );