:: deftheorem REACH defines -reachable MSAFREE5:def 33 :
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S holds
( s2 is s1 -reachable iff TranslationRel S reduces s1,s2 );