let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a being Element of S st S is (R1) & S is (R4) holds
((1. S) ") * a <<>> a
let a be Element of S; :: thesis: ( S is (R1) & S is (R4) implies ((1. S) ") * a <<>> a )
assume A1: ( S is (R1) & S is (R4) ) ; :: thesis: ((1. S) ") * a <<>> a
take ((1. S) ") * ((1. S) * a) ; :: according to ABSRED_0:def 20 :: thesis: ( ((1. S) ") * a <=*= ((1. S) ") * ((1. S) * a) & ((1. S) ") * ((1. S) * a) =*=> a )
(1. S) * a ==> a by A1;
hence ((1. S) ") * ((1. S) * a) =*=> ((1. S) ") * a by Th2, ThI3; :: thesis: ((1. S) ") * ((1. S) * a) =*=> a
thus ((1. S) ") * ((1. S) * a) =*=> a by A1, Th2; :: thesis: verum