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

a * ((a ") * b) <<>> b

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

assume A1: ( S is (R1) & S is (R3) & S is (R11) ) ; :: 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;

hence (a * (a ")) * b =*=> b by Lem3; :: thesis: verum

a * ((a ") * b) <<>> b

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

assume A1: ( S is (R1) & S is (R3) & S is (R11) ) ; :: 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;

hence (a * (a ")) * b =*=> b by Lem3; :: thesis: verum