let x, y be object ; :: 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 Th15;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) ) by A1; :: thesis: verum