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