let X be set ; :: thesis: ( X is constituted-FinTrees implies X is constituted-Trees )
assume X is constituted-FinTrees ; :: thesis: X is constituted-Trees
hence for x being set st x in X holds
x is Tree by Def4; :: according to TREES_3:def 3 :: thesis: verum