let X, Y be set ; :: thesis: ( X is constituted-DTrees implies ( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees ) )
assume A1: for x being object st x in X holds
x is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: ( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )
thus X /\ Y is constituted-DTrees :: thesis: ( Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )

proof

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 x in X by XBOOLE_0:def 4;
hence x is DecoratedTree by A1; :: thesis: verum

end;

hence Y /\ X is constituted-DTrees ; :: 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
hence x is DecoratedTree by A1; :: thesis: verum