consider T being DecoratedTree;
take {T} ; :: thesis: ( {T} is finite & {T} is constituted-DTrees & not {T} is empty )
thus ( {T} is finite & {T} is constituted-DTrees & not {T} is empty ) by Th15; :: thesis: verum