let x be set ; :: according to TREES_3:def 4 :: thesis: ( x in FinTrees implies x is finite Tree )
thus ( x in FinTrees implies x is finite Tree ) by Def2; :: thesis: verum