:: deftheorem defines ==> LANG1:def 1 :
for G being non empty DTConstrStr
for s being Symbol of G
for n being FinSequence holds
( s ==> n iff [s,n] in the Rules of G );