theorem :: LANG1:9

for G being non empty GrammarStr
for n being String of G holds
( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )