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