let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra implies for x, y being Element of X st x \ y = x holds
y \ x = y )
assume A1: X is commutative BCK-algebra ; :: thesis: for x, y being Element of X st x \ y = x holds
y \ x = y
let x, y be Element of X; :: thesis: ( x \ y = x implies y \ x = y )
assume x \ y = x ; :: thesis: y \ x = y
then y \ (y \ x) = x \ x by A1, Def1
.= 0. X by BCIALG_1:def 5 ;
then y \ x = y \ (0. X) by BCIALG_1:8
.= y by BCIALG_1:2 ;
hence y \ x = y ; :: thesis: verum