nt ==> roots p by Def6;
hence nt -tree p is Element of TS G by Def1; :: thesis: verum