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 )
C1: ( 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 A: 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 A2: (x \ (y \ x)) \ (0. X) in I by BCIALG_1:2;
0. X in I by A, Def2;
hence x in I by A, A2, Def2; :: thesis: verum

end;

( ( 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 B: for x, y being Element of X st x \ (y \ x) in I holds
x in I ; :: thesis: I is implicative-ideal of X
D: 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 B; :: thesis: verum

end;

0. X in I by BCIALG_1:def 18;
hence I is implicative-ideal of X by Def2, D; :: 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 C1; :: thesis: verum