for S being non empty partial quasi_total non-empty Group-like invariant TRSStr st S is (R5) & S is (R8) holds
(1. S) " <<>> 1. S