theorem Th32: :: TREES_3:32

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