let X be BCK-algebra; :: thesis: ( {(0. X)} is commutative Ideal of X implies ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) )

assume {(0. X)} is commutative Ideal of X ; :: thesis: ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )

then A1: X is commutative BCK-algebra by Th36;
hence for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; :: thesis: ( ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )

thus for x, y being Element of X st x \ y = x holds
y \ x = y by ; :: thesis: ( ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )

thus for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x by ; :: thesis: ( ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )

thus for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by ; :: thesis: for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y)

thus for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by ; :: thesis: verum