let X be BCK-algebra; :: thesis: for I being Ideal of X holds

( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I )

let I be Ideal of X; :: thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I )

A1: 0. X in I by BCIALG_1:def 18;

thus ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I ) by Def8; :: 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 I is positive-implicative-ideal of X )

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

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

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

( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I )

let I be Ideal of X; :: thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I )

A1: 0. X in I by BCIALG_1:def 18;

thus ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I ) by Def8; :: 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 I is positive-implicative-ideal of X )

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

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

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