set s = the Symbol of G;

per cases ( for tnt being FinSequence holds not the Symbol of G ==> tnt or ex tnt being FinSequence st the Symbol of G ==> tnt ) ;

suppose for tnt being FinSequence holds not the Symbol of G ==> tnt ; :: thesis: not TS G is empty

then the Symbol of G in { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } ;
then the Symbol of G in Terminals G by LANG1:def 2;
hence not TS G is empty by Def1; :: thesis: verum

end;

suppose ex tnt being FinSequence st the Symbol of G ==> tnt ; :: thesis: not TS G is empty

then the Symbol of G in { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } ;
then the Symbol of G in NonTerminals G by LANG1:def 3;
then ex p being FinSequence of TS G st the Symbol of G ==> roots p by Def5;
hence not TS G is empty by Def1; :: thesis: verum

end;

end;