let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a, b being Element of S st S is (R1) & S is (R2) & S is (R3) holds
(a ") * (a * b) <<>> b
let a, b be Element of S; :: thesis: ( S is (R1) & S is (R2) & S is (R3) implies (a ") * (a * b) <<>> b )
assume A1: ( S is (R1) & S is (R2) & S is (R3) ) ; :: thesis: (a ") * (a * b) <<>> b
take ((a ") * a) * b ; :: according to ABSRED_0:def 20 :: thesis: ( (a ") * (a * b) <=*= ((a ") * a) * b & ((a ") * a) * b =*=> b )
thus ((a ") * a) * b =*=> (a ") * (a * b) by A1, Th2; :: thesis: ((a ") * a) * b =*=> b
( ((a ") * a) * b ==> (1. S) * b & (1. S) * b ==> b ) by A1, ThI2;
then ( ((a ") * a) * b =*=> (1. S) * b & (1. S) * b =*=> b ) by Th2;
hence ((a ") * a) * b =*=> b by Th3; :: thesis: verum