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

proof

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

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

end;

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

end;

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