let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a being Element of S st S is (R6) & S is (R8) holds

(a ") " <<>> a

let a be Element of S; :: thesis: ( S is (R6) & S is (R8) implies (a ") " <<>> a )

assume A1: ( S is (R6) & S is (R8) ) ; :: thesis: (a ") " <<>> a

take ((a ") ") * (1. S) ; :: according to ABSRED_0:def 20 :: thesis: ( (a ") " <=*= ((a ") ") * (1. S) & ((a ") ") * (1. S) =*=> a )

thus ((a ") ") * (1. S) =*=> (a ") " by A1, Th2; :: thesis: ((a ") ") * (1. S) =*=> a

thus ((a ") ") * (1. S) =*=> a by A1, Th2; :: thesis: verum

(a ") " <<>> a

let a be Element of S; :: thesis: ( S is (R6) & S is (R8) implies (a ") " <<>> a )

assume A1: ( S is (R6) & S is (R8) ) ; :: thesis: (a ") " <<>> a

take ((a ") ") * (1. S) ; :: according to ABSRED_0:def 20 :: thesis: ( (a ") " <=*= ((a ") ") * (1. S) & ((a ") ") * (1. S) =*=> a )

thus ((a ") ") * (1. S) =*=> (a ") " by A1, Th2; :: thesis: ((a ") ") * (1. S) =*=> a

thus ((a ") ") * (1. S) =*=> a by A1, Th2; :: thesis: verum