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 (R12) & S is (R15) holds

a * ((b * a) ") =*=> b "

let a, b be Element of S; :: thesis: ( S is (R12) & S is (R15) implies a * ((b * a) ") =*=> b " )

assume A1: ( S is (R12) & S is (R15) ) ; :: thesis: a * ((b * a) ") =*=> b "

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

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

a * ((b * a) ") =*=> b "

let a, b be Element of S; :: thesis: ( S is (R12) & S is (R15) implies a * ((b * a) ") =*=> b " )

assume A1: ( S is (R12) & S is (R15) ) ; :: thesis: a * ((b * a) ") =*=> b "

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

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