theorem Th29: :: TREES_3:29

for x being object holds
( <*x*> is FinTree-yielding iff x is finite Tree )