let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative )

assume A1: for x, y being Element of X holds y \ x = x \ y ; :: thesis: X is associative

let x, y, z be Element of X; :: according to BCIALG_1:def 20 :: thesis: (x \ y) \ z = x \ (y \ z)

x \ (y \ z) = (y \ z) \ x by A1

.= (y \ x) \ z by Th7 ;

hence (x \ y) \ z = x \ (y \ z) by A1; :: thesis: verum

assume A1: for x, y being Element of X holds y \ x = x \ y ; :: thesis: X is associative

let x, y, z be Element of X; :: according to BCIALG_1:def 20 :: thesis: (x \ y) \ z = x \ (y \ z)

x \ (y \ z) = (y \ z) \ x by A1

.= (y \ x) \ z by Th7 ;

hence (x \ y) \ z = x \ (y \ z) by A1; :: thesis: verum