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