let x, y be set ; :: thesis: ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )
( ( x is DecoratedTree & y is DecoratedTree implies {x,y} is constituted-DTrees ) & ( {x,y} is constituted-DTrees implies ( x is DecoratedTree & y is DecoratedTree ) ) & rng <*x,y*> = {x,y} ) by Th18, FINSEQ_2:147;
hence ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) ) by Def11; :: thesis: verum