let X be BCK-algebra; :: thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
let IT be non empty Subset of X; :: thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT )
assume A1: IT is Commutative-Ideal of X ; :: thesis: for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
let x, y be Element of X; :: thesis: ( x \ y in IT implies x \ (y \ (y \ x)) in IT )
assume x \ y in IT ; :: thesis: x \ (y \ (y \ x)) in IT
then A2: (x \ y) \ (0. X) in IT by BCIALG_1:2;
thus x \ (y \ (y \ x)) in IT by A1, A2, Def10; :: thesis: verum