theorem :: TREES_3:2

for X being set holds
( X is constituted-FinTrees iff X c= FinTrees )