let X be BCK-algebra; :: thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let I be Ideal of X; :: thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) implies for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
assume A1: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ; :: thesis: for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I implies (x \ z) \ (y \ z) in I )
((x \ (y \ z)) \ (x \ y)) \ (y \ (y \ z)) = 0. X by BCIALG_1:1;
then (x \ (y \ z)) \ (x \ y) <= y \ (y \ z) ;
then A2: ((x \ (y \ z)) \ (x \ y)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;
(y \ (y \ z)) \ z = (y \ z) \ (y \ z) by BCIALG_1:7;
then ((x \ (y \ z)) \ (x \ y)) \ z <= 0. X by A2, BCIALG_1:def 5;
then (((x \ (y \ z)) \ (x \ y)) \ z) \ (0. X) = 0. X ;
then ((x \ (y \ z)) \ (x \ y)) \ z = 0. X by BCIALG_1:2;
then A3: ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:def 18;
assume (x \ y) \ z in I ; :: thesis: (x \ z) \ (y \ z) in I
then (x \ (y \ z)) \ z in I by A1, A3;
hence (x \ z) \ (y \ z) in I by BCIALG_1:7; :: thesis: verum