set T = the finite Tree;
take <* the finite Tree*> ; :: thesis: ( <* the finite Tree*> is Tree-yielding & <* the finite Tree*> is FinTree-yielding & not <* the finite Tree*> is empty )
thus ( <* the finite Tree*> is Tree-yielding & <* the finite Tree*> is FinTree-yielding & not <* the finite Tree*> is empty ) by Th28, Th29; :: thesis: verum