take G = EmptyGrammar 0 ; :: thesis: ( G is efective & G is finite )
A1: ( the carrier of G = {0 } & the Rules of G = {[0 ,{} ]} ) by Def7;
thus G is efective :: thesis: G is finite

proof

thus not Lang G is empty by Th11; :: according to LANG1:def 11 :: thesis: ( the InitialSym of G in NonTerminals G & ( 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 ) ) )
( the InitialSym of G = 0 & {} = {} the carrier of G & [0 ,{} ] in {[0 ,{} ]} ) by A1, TARSKI:def 1;
then ( the InitialSym of G ==> <*> the carrier of G & NonTerminals G = { s where s is Symbol of G : ex n being FinSequence st s ==> n } ) by A1, Def1;
hence the InitialSym of G in NonTerminals G ; :: thesis: 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 )
thus 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; :: thesis: verum

end;

thus the Rules of G is finite by A1; :: according to LANG1:def 12 :: thesis: verum