:: deftheorem defines (R15) ABSRED_0:def 50 :
for S being non empty partial quasi_total non-empty Group-like TRSStr holds
( S is (R15) iff for a, b being Element of S holds (a * b) " ==> (b ") * (a ") );