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