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 )

x in I )

x in I ) by A1; :: thesis: verum

( 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

( I is implicative-ideal of X implies for x, y being Element of X st x \ (y \ x) in I holds
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

hence I is implicative-ideal of X by A3, Def7; :: thesis: verum

end;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

0. X in I
by BCIALG_1:def 18;
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;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

hence I is implicative-ideal of X by A3, Def7; :: thesis: verum

x in I )

proof

hence
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
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;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

x in I ) by A1; :: thesis: verum