let X be BCK-algebra; :: thesis:
let I be Ideal of X; :: thesis:
thus ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) :: thesis:

end;

assume A3: for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ; :: thesis:
A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I

let x, y, z be Element of X; :: thesis:
assume that
A5: (x \ y) \ z in I and
A6: y \ z in I ; :: thesis:
(((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def 3;
then ((x \ z) \ z) \ ((x \ y) \ z) <= (x \ z) \ (x \ y) ;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= 0. X by BCIALG_1:1;
then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X ;
then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2;
then ((x \ z) \ z) \ ((x \ y) \ z) <= y \ z ;
then ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5;
then (x \ z) \ z in I by A5, BCIALG_1:def 18;
hence x \ z in I by A3; :: thesis:

end;

end;