let x, y be set ; :: thesis: ( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )
thus ( {x,y} is constituted-DTrees implies ( x is DecoratedTree & y is DecoratedTree ) ) :: thesis: ( x is DecoratedTree & y is DecoratedTree implies {x,y} is constituted-DTrees )

proof

assume A1: for z being set st z in {x,y} holds
z is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: ( x is DecoratedTree & y is DecoratedTree )
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence ( x is DecoratedTree & y is DecoratedTree ) by A1; :: thesis: verum

end;

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