set t = the finite DecoratedTree;
take <* the finite DecoratedTree*> ; :: thesis: ( <* the finite DecoratedTree*> is finite-yielding & <* the finite DecoratedTree*> is DTree-yielding & not <* the finite DecoratedTree*> is empty )
thus <* the finite DecoratedTree*> is finite-yielding :: thesis: ( <* the finite DecoratedTree*> is DTree-yielding & not <* the finite DecoratedTree*> is empty )

proof

now :: thesis: for x being set st x in rng <* the finite DecoratedTree*> holds
x is finite

let x be set ; :: thesis: ( x in rng <* the finite DecoratedTree*> implies x is finite )
assume x in rng <* the finite DecoratedTree*> ; :: thesis: x is finite
then x in { the finite DecoratedTree} by FINSEQ_1:39;
hence x is finite ; :: thesis: verum

end;

hence <* the finite DecoratedTree*> is finite-yielding ; :: thesis: verum

end;

thus ( <* the finite DecoratedTree*> is DTree-yielding & not <* the finite DecoratedTree*> is empty ) ; :: thesis: verum