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 (R10) holds
((1. S) ") * a =*=> a
let a be Element of S; :: thesis: ( S is (R1) & S is (R10) implies ((1. S) ") * a =*=> a )
assume A1: ( S is (R1) & S is (R10) ) ; :: thesis: ((1. S) ") * a =*=> a
( ((1. S) ") * a ==> (1. S) * a & (1. S) * a ==> a ) by A1, ThI2;
hence ((1. S) ") * a =*=> a by Lem3; :: thesis: verum