theorem :: TREES_3:21

for D being non empty set holds FinTrees D c= Trees D by Def7;