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 (R3) & S is (R11) holds

a * (b * ((a * b) ")) <<>> 1. S

let a, b be Element of S; :: thesis: ( S is (R3) & S is (R11) implies a * (b * ((a * b) ")) <<>> 1. S )

assume A1: ( S is (R3) & S is (R11) ) ; :: thesis: a * (b * ((a * b) ")) <<>> 1. S

take (a * b) * ((a * b) ") ; :: according to ABSRED_0:def 20 :: thesis: ( a * (b * ((a * b) ")) <=*= (a * b) * ((a * b) ") & (a * b) * ((a * b) ") =*=> 1. S )

thus (a * b) * ((a * b) ") =*=> a * (b * ((a * b) ")) by A1, Th2; :: thesis: (a * b) * ((a * b) ") =*=> 1. S

thus (a * b) * ((a * b) ") =*=> 1. S by A1, Th2; :: thesis: verum

a * (b * ((a * b) ")) <<>> 1. S

let a, b be Element of S; :: thesis: ( S is (R3) & S is (R11) implies a * (b * ((a * b) ")) <<>> 1. S )

assume A1: ( S is (R3) & S is (R11) ) ; :: thesis: a * (b * ((a * b) ")) <<>> 1. S

take (a * b) * ((a * b) ") ; :: according to ABSRED_0:def 20 :: thesis: ( a * (b * ((a * b) ")) <=*= (a * b) * ((a * b) ") & (a * b) * ((a * b) ") =*=> 1. S )

thus (a * b) * ((a * b) ") =*=> a * (b * ((a * b) ")) by A1, Th2; :: thesis: (a * b) * ((a * b) ") =*=> 1. S

thus (a * b) * ((a * b) ") =*=> 1. S by A1, Th2; :: thesis: verum