let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) )
assume A1: X is commutative BCK-algebra ; :: thesis: for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X )
A2: for x, y being Element of X st y \ (y \ x) = 0. X holds
x \ y = x

proof

let x, y be Element of X; :: thesis: ( y \ (y \ x) = 0. X implies x \ y = x )
assume A3: y \ (y \ x) = 0. X ; :: thesis: x \ y = x
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (0. X) by A1, A3, Def1
.= x by BCIALG_1:2 ;
hence x \ y = x ; :: thesis: verum

end;

for x, y being Element of X st x \ y = x holds
y \ (y \ x) = 0. X

proof

let x, y be Element of X; :: thesis: ( x \ y = x implies y \ (y \ x) = 0. X )
assume x \ y = x ; :: thesis: y \ (y \ x) = 0. X
then y \ (y \ x) = x \ x by A1, Def1
.= 0. X by BCIALG_1:def 5 ;
hence y \ (y \ x) = 0. X ; :: thesis: verum

end;

hence for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by A2; :: thesis: verum