:: deftheorem Def3 defines with_terminals DTCONSTR:def 3 :
for G being non empty DTConstrStr holds
( G is with_terminals iff Terminals G <> {} );