let Y be Subset of X; :: thesis: Y is constituted-DTrees
let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in Y implies x is DecoratedTree )
thus ( x in Y implies x is DecoratedTree ) by Def5; :: thesis: verum