consider s being Symbol of G;

per cases ( for tnt being FinSequence holds not s ==> tnt or ex tnt being FinSequence st s ==> tnt ) ;

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

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

end;

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

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

end;

end;