let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: ( S is (R5) & S is (R8) implies (1. S) " <<>> 1. S )
assume A1: ( S is (R5) & S is (R8) ) ; :: thesis: (1. S) " <<>> 1. S
take ((1. S) ") * (1. S) ; :: according to ABSRED_0:def 20 :: thesis: ( (1. S) " <=*= ((1. S) ") * (1. S) & ((1. S) ") * (1. S) =*=> 1. S )
thus ((1. S) ") * (1. S) =*=> (1. S) " by A1, Th2; :: thesis: ((1. S) ") * (1. S) =*=> 1. S
thus ((1. S) ") * (1. S) =*=> 1. S by A1, Th2; :: thesis: verum