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

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