theorem Th13: :: TREES_3:13

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