:: deftheorem defines NonTerminals LANG1:def 3 :
for G being non empty DTConstrStr holds NonTerminals G = { s where s is Symbol of G : ex n being FinSequence st s ==> n } ;