theorem Th9: :: TREES_3:9

for X, Y being set holds
( ( X is constituted-DTrees & Y is constituted-DTrees ) iff X \/ Y is constituted-DTrees )