defpred S₂[ Element of G] means ex tnt being FinSequence st $1 ==> tnt;
{ t where t is Element of G : S₂[t] } c= the carrier of G from FRAENKEL:sch 10();
hence NonTerminals G is non empty Subset of G by Def4, LANG1:def 3; :: thesis: verum