:: deftheorem Def5 defines with_useful_nonterminals DTCONSTR:def 5 :
for G being non empty DTConstrStr holds
( G is with_useful_nonterminals iff for nt being Symbol of G st nt in NonTerminals G holds
ex p being FinSequence of TS G st nt ==> roots p );