consider T being finite Tree;
take <*T*> ; :: thesis: ( <*T*> is Tree-yielding & <*T*> is FinTree-yielding & not <*T*> is empty )
thus ( <*T*> is Tree-yielding & <*T*> is FinTree-yielding & not <*T*> is empty ) by Th30, Th31; :: thesis: verum