:: deftheorem Def2 defines FinTrees TREES_3:def 2 :
for b₁ being Subset of Trees holds
( b₁ = FinTrees iff for x being object holds
( x in b₁ iff x is finite Tree ) );