0 |-> T = {} ;
hence n |-> T is DTree-yielding by Th36; :: thesis: verum