let x be object ; :: thesis: ( {x} is constituted-DTrees iff x is DecoratedTree )
thus ( {x} is constituted-DTrees implies x is DecoratedTree ) :: thesis: ( x is DecoratedTree implies {x} is constituted-DTrees )

proof

assume A1: for y being object st y in {x} holds
y is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: x is DecoratedTree
x in {x} by TARSKI:def 1;
hence x is DecoratedTree by A1; :: thesis: verum

end;

assume A2: x is DecoratedTree ; :: thesis: {x} is constituted-DTrees
let y be object ; :: according to TREES_3:def 5 :: thesis: ( y in {x} implies y is DecoratedTree )
thus ( y in {x} implies y is DecoratedTree ) by A2, TARSKI:def 1; :: thesis: verum