FinTrees is constituted-FinTrees

proof

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

end;

hence FinTrees is constituted-FinTrees ; :: thesis: verum