theorem Th16: :: TREES_3:16

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