theorem Th31: :: TREES_3:31

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