for S being non empty partial quasi_total non-empty Group-like invariant TRSStr
for a, b being Element of S st S is (R1) & S is (R3) & S is (R6) holds
((a ") ") * b <<>> a * b