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 holds

(x \ z) \ (y \ z) in I ) holds

I is positive-implicative-ideal of X

let I be Ideal of X; :: thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds

(x \ z) \ (y \ z) in I ) implies I is positive-implicative-ideal of X )

assume A1: for x, y, z being Element of X st (x \ y) \ z in I holds

(x \ z) \ (y \ z) in I ; :: thesis: I is positive-implicative-ideal of X

A2: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I

hence I is positive-implicative-ideal of X by A2, Def8; :: thesis: verum

(x \ z) \ (y \ z) in I ) holds

I is positive-implicative-ideal of X

let I be Ideal of X; :: thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds

(x \ z) \ (y \ z) in I ) implies I is positive-implicative-ideal of X )

assume A1: for x, y, z being Element of X st (x \ y) \ z in I holds

(x \ z) \ (y \ z) in I ; :: thesis: I is positive-implicative-ideal of X

A2: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I

proof

0. X in I
by BCIALG_1:def 18;
let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )

assume that

A3: (x \ y) \ z in I and

A4: y \ z in I ; :: thesis: x \ z in I

(x \ z) \ (y \ z) in I by A1, A3;

hence x \ z in I by A4, BCIALG_1:def 18; :: thesis: verum

end;assume that

A3: (x \ y) \ z in I and

A4: y \ z in I ; :: thesis: x \ z in I

(x \ z) \ (y \ z) in I by A1, A3;

hence x \ z in I by A4, BCIALG_1:def 18; :: thesis: verum

hence I is positive-implicative-ideal of X by A2, Def8; :: thesis: verum