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 ex b₁ being Subset of Trees st
( b₁ is constituted-FinTrees & not b₁ is empty ) ; :: thesis: verum