set T = the DecoratedTree;
take { the DecoratedTree} ; :: thesis: ( { the DecoratedTree} is finite & { the DecoratedTree} is constituted-DTrees & not { the DecoratedTree} is empty )
thus ( { the DecoratedTree} is finite & { the DecoratedTree} is constituted-DTrees & not { the DecoratedTree} is empty ) by Th14; :: thesis: verum