let a be set ; :: thesis: Terminals (EmptyGrammar a) = {}
set E = EmptyGrammar a;
set b = the Element of Terminals (EmptyGrammar a);
the Rules of (EmptyGrammar a) = {[a,{}]} by Def7;
then A1: [a,{}] in the Rules of (EmptyGrammar a) by TARSKI:def 1;
assume not Terminals (EmptyGrammar a) = {} ; :: thesis: contradiction
then the Element of Terminals (EmptyGrammar a) in Terminals (EmptyGrammar a) ;
then consider s being Symbol of (EmptyGrammar a) such that
the Element of Terminals (EmptyGrammar a) = s and
A2: for n being FinSequence holds not s ==> n ;
the carrier of (EmptyGrammar a) = {a} by Def7;
then s = a by TARSKI:def 1;
then s ==> <*> the carrier of (EmptyGrammar a) by A1;
hence contradiction by A2; :: thesis: verum