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