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