let x, y be object ; :: thesis: ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )
A1: ( ( x is DecoratedTree & y is DecoratedTree ) iff {x,y} is constituted-DTrees ) by Th17;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) ) by A1; :: thesis: verum