defpred S₂[ Element of G] means for tnt being FinSequence holds not $1 ==> tnt;
{ t where t is Element of G : S₂[t] } c= the carrier of G from FRAENKEL:sch 10();
hence Terminals G is non empty Subset of G by Def3, LANG1:def 2; :: thesis: verum