consider T being DecoratedTree;
take <*T*> ; :: thesis: ( <*T*> is DTree-yielding & not <*T*> is empty )
thus ( <*T*> is DTree-yielding & not <*T*> is empty ) by Th32; :: thesis: verum