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