theorem Th6: :: TREES_3:6
for X, Y being set holds
( ( X is constituted-FinTrees & Y is constituted-FinTrees ) iff X \/ Y is constituted-FinTrees )