:: deftheorem Def4 defines with_nonterminals DTCONSTR:def 4 :
for G being non empty DTConstrStr holds
( G is with_nonterminals iff NonTerminals G <> {} );