let X, Y be set ; :: thesis: ( X is constituted-DTrees & Y is constituted-DTrees implies X \+\ Y is constituted-DTrees )
assume that
A1: for x being object st x in X holds
x is DecoratedTree and
A2: for x being object st x in Y holds
x is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: X \+\ Y is constituted-DTrees
let x be object ; :: according to TREES_3:def 5 :: thesis: ( x in X \+\ Y implies x is DecoratedTree )
assume x in X \+\ Y ; :: thesis: x is DecoratedTree
then ( not x in X iff x in Y ) by XBOOLE_0:1;
hence x is DecoratedTree by A1, A2; :: thesis: verum