let X be quasi-commutative BCK-algebra; :: thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y )
thus ( X is BCK-algebra of 0 ,1, 0 ,1 implies for x, y being Element of X holds x \ y = (x \ y) \ y ) :: thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ y ) implies X is BCK-algebra of 0 ,1, 0 ,1 )

proof

assume A1: X is BCK-algebra of 0 ,1, 0 ,1 ; :: thesis: for x, y being Element of X holds x \ y = (x \ y) \ y
for x, y being Element of X holds x \ y = (x \ y) \ y

proof

let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y
A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A3: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
A4: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8
.= x \ y by A2, BCIALG_1:2 ;
A5: Polynom 0 ,1,x,(x \ y) = Polynom 0 ,1,(x \ y),x by A1, Def3;
(x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x,(x \ (x \ y)) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2
.= ((x \ y),((x \ y) \ x) to_power 1),(x \ (x \ y)) to_power 1 by A5, BCIALG_2:2
.= ((x \ y) \ ((x \ y) \ x)),(x \ (x \ y)) to_power 1 by BCIALG_2:2
.= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ;
hence x \ y = (x \ y) \ y by A4, A3; :: thesis: verum

end;

hence for x, y being Element of X holds x \ y = (x \ y) \ y ; :: thesis: verum

end;

assume for x, y being Element of X holds x \ y = (x \ y) \ y ; :: thesis: X is BCK-algebra of 0 ,1, 0 ,1
then X is BCK-positive-implicative BCK-algebra by BCIALG_3:28;
hence X is BCK-algebra of 0 ,1, 0 ,1 by Th49; :: thesis: verum