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

proof

assume A2: for x, y being Element of X st x \ (y \ x) in I holds
x in I ; :: thesis: I is implicative-ideal of X
A3: for x, y, z being Element of X st (x \ (y \ x)) \ z in I & z in I holds
x in I

proof

let x, y, z be Element of X; :: thesis: ( (x \ (y \ x)) \ z in I & z in I implies x in I )
assume ( (x \ (y \ x)) \ z in I & z in I ) ; :: thesis: x in I
then x \ (y \ x) in I by BCIALG_1:def 18;
hence x in I by A2; :: thesis: verum

end;

0. X in I by BCIALG_1:def 18;
hence I is implicative-ideal of X by A3, Def7; :: thesis: verum

end;

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

proof

assume A4: I is implicative-ideal of X ; :: thesis: for x, y being Element of X st x \ (y \ x) in I holds
x in I
let x, y be Element of X; :: thesis: ( x \ (y \ x) in I implies x in I )
assume x \ (y \ x) in I ; :: thesis: x in I
then A5: (x \ (y \ x)) \ (0. X) in I by BCIALG_1:2;
thus x in I by A4, A5, Def7; :: thesis: verum

end;

hence ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I ) by A1; :: thesis: verum