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