:: deftheorem Def11 defines effective LANG1:def 11 :
for IT being non empty GrammarStr holds
( IT is effective iff ( not Lang IT is empty & the InitialSym of IT in NonTerminals IT & ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT & s in rng p ) ) ) );