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 holds
(x \ z) \ (y \ 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 holds
(x \ z) \ (y \ z) in I )
( 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;
hence ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) by Th52, Th53; :: thesis: verum