let T be DTree-set of D; :: thesis: T is constituted-DTrees
let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in T implies x is DecoratedTree )
thus ( x in T implies x is DecoratedTree ) by Def6; :: thesis: verum