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