theorem :: TREES_3:19

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