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 (R14) holds
(a * b) " <<>> (b ") * (a ")
let a, b be Element of S; :: thesis: ( S is (R4) & S is (R14) implies (a * b) " <<>> (b ") * (a ") )
assume A1: ( S is (R4) & S is (R14) ) ; :: thesis: (a * b) " <<>> (b ") * (a ")
take (b ") * (b * ((a * b) ")) ; :: according to ABSRED_0:def 20 :: thesis: ( (a * b) " <=*= (b ") * (b * ((a * b) ")) & (b ") * (b * ((a * b) ")) =*=> (b ") * (a ") )
thus (b ") * (b * ((a * b) ")) =*=> (a * b) " by A1, Th2; :: thesis: (b ") * (b * ((a * b) ")) =*=> (b ") * (a ")
b * ((a * b) ") ==> a " by A1;
hence (b ") * (b * ((a * b) ")) =*=> (b ") * (a ") by Th2, ThI3; :: thesis: verum