for x being object holds
( {x} is constituted-FinTrees iff x is finite Tree )