:: deftheorem defines ==> LANG1:def 4 :
for G being non empty DTConstrStr
for n, m being String of G holds
( n ==> m iff ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 & m = (n1 ^ n3) ^ n2 & s ==> n3 ) );