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