let Y be Subset of X; :: thesis: Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def 4 :: thesis: ( x in Y implies x is finite Tree )
thus ( x in Y implies x is finite Tree ) by Def4; :: thesis: verum