theorem :: TREES_3:20

for X, Y being set st X is constituted-DTrees & Y c= X holds
Y is constituted-DTrees ;