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