:: deftheorem defines " ABSRED_0:def 34 :
for S being non empty partial quasi_total non-empty Group-like TRSStr
for a being Element of S holds a " = (Den ((In (2,(dom the charact of S))),S)) . <*a*>;