let G be non empty GrammarStr ; :: thesis: 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*> ) )
let n be String of G; :: thesis: ( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )

now :: thesis: ( n in Lang G implies ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) )

assume n in Lang G ; :: thesis: ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> )
then ex a being Element of the carrier of G * st
( n = a & rng a c= Terminals G & a is_derivable_from <* the InitialSym of G*> ) ;
hence ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) ; :: thesis: verum

end;

hence ( n in Lang G iff ( rng n c= Terminals G & n is_derivable_from <* the InitialSym of G*> ) ) ; :: thesis: verum