theorem :: TREES_3:18
for X, Y being set st X is constituted-Trees & Y c= X holds
Y is constituted-Trees ;