take G = EmptyGrammar 0; :: thesis: ( G is effective & G is finite )
A1: the Rules of G = {[0,{}]} by Def7;
the carrier of G = {0} by Def7;
then A2: the InitialSym of G = 0 by TARSKI:def 1;
[0,{}] in {[0,{}]} by TARSKI:def 1;
then the InitialSym of G ==> <*> the carrier of G by A1, A2;
then A3: the InitialSym of G in NonTerminals G ;
A4: for s being Symbol of G st s in Terminals G holds
ex p being String of G st
( p in Lang G & s in rng p ) by Th10;
not Lang G is empty by Th11;
hence G is effective by A3, A4; :: thesis: G is finite
thus the Rules of G is finite by A1; :: according to LANG1:def 12 :: thesis: verum