theorem :: TREES_3:7

for X, Y being set st X is constituted-FinTrees & Y is constituted-FinTrees holds
X \+\ Y is constituted-FinTrees