theorem :: TREES_3:11
for X, Y being set st X is constituted-DTrees holds
( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )