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 (R4) & S is (R8) & S is (R13) holds

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

let a, b be Element of S; :: thesis: ( S is (R4) & S is (R8) & S is (R13) implies a * ((b * a) ") <<>> b " )

assume A1: ( S is (R4) & S is (R8) & S is (R13) ) ; :: thesis: a * ((b * a) ") <<>> b "

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

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

( (b ") * (b * (a * ((b * a) "))) ==> (b ") * (1. S) & (b ") * (1. S) ==> b " ) by A1, ThI3;

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

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

let a, b be Element of S; :: thesis: ( S is (R4) & S is (R8) & S is (R13) implies a * ((b * a) ") <<>> b " )

assume A1: ( S is (R4) & S is (R8) & S is (R13) ) ; :: thesis: a * ((b * a) ") <<>> b "

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

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

( (b ") * (b * (a * ((b * a) "))) ==> (b ") * (1. S) & (b ") * (1. S) ==> b " ) by A1, ThI3;

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