:: deftheorem defines 1. ABSRED_0:def 33 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds 1. S = (Den ((In (1,(dom the charact of S))),S)) . {};