:: deftheorem defines Lang LANG1:def 6 :
for G being non empty GrammarStr holds Lang G = { a where a is Element of the carrier of G * : ( rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) } ;