let x, y be set ; :: thesis: ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) )
( ( x is Tree & y is Tree implies {x,y} is constituted-Trees ) & ( {x,y} is constituted-Trees implies ( x is Tree & y is Tree ) ) & rng <*x,y*> = {x,y} ) by Th16, FINSEQ_2:147;
hence ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) ) by Def9; :: thesis: verum