let x, y be object ; :: 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 object st z in {x,y} holds
z is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: ( x is DecoratedTree & y is DecoratedTree )
A2: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence ( x is DecoratedTree & y is DecoratedTree ) by A1, A2; :: thesis: verum

end;

assume that
A3: x is DecoratedTree and
A4: y is DecoratedTree ; :: thesis: {x,y} is constituted-DTrees
let z be object ; :: 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 A3, A4, TARSKI:def 2; :: thesis: verum