set T = the DecoratedTree;
take <* the DecoratedTree*> ; :: thesis: ( <* the DecoratedTree*> is DTree-yielding & not <* the DecoratedTree*> is empty )
thus ( <* the DecoratedTree*> is DTree-yielding & not <* the DecoratedTree*> is empty ) by Th30; :: thesis: verum