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

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

x \ (y \ z) in I )

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

x \ (y \ z) in I )

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

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

x \ (y \ z) in I ) implies I is associative-ideal of X )

x \ (y \ z) in I ; :: thesis: I is associative-ideal of X

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

x in I

hence I is associative-ideal of X by A5, Def4; :: thesis: verum

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

x \ (y \ z) in I )

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

x \ (y \ z) in I )

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

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

x \ (y \ z) in I ) implies I is associative-ideal of X )

proof

assume A4:
for x, y, z being Element of X st (x \ y) \ z in I holds
assume A1:
I is associative-ideal of X
; :: thesis: for x, y, z being Element of X st (x \ y) \ z in I holds

x \ (y \ z) in I

let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I implies x \ (y \ z) in I )

assume A2: (x \ y) \ z in I ; :: thesis: x \ (y \ z) in I

(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;

then x \ (x \ y) <= y ;

then (x \ (x \ y)) \ (y \ z) <= y \ (y \ z) by BCIALG_1:5;

then A3: ((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;

(y \ (y \ z)) \ z = 0. X by BCIALG_1:1;

then (((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X by A3;

then ((x \ (x \ y)) \ (y \ z)) \ z = 0. X by BCIALG_1:2;

then ((x \ (x \ y)) \ (y \ z)) \ z in I by A1, Def4;

then ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:7;

hence x \ (y \ z) in I by A1, A2, Def4; :: thesis: verum

end;x \ (y \ z) in I

let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I implies x \ (y \ z) in I )

assume A2: (x \ y) \ z in I ; :: thesis: x \ (y \ z) in I

(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;

then x \ (x \ y) <= y ;

then (x \ (x \ y)) \ (y \ z) <= y \ (y \ z) by BCIALG_1:5;

then A3: ((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;

(y \ (y \ z)) \ z = 0. X by BCIALG_1:1;

then (((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X by A3;

then ((x \ (x \ y)) \ (y \ z)) \ z = 0. X by BCIALG_1:2;

then ((x \ (x \ y)) \ (y \ z)) \ z in I by A1, Def4;

then ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:7;

hence x \ (y \ z) in I by A1, A2, Def4; :: thesis: verum

x \ (y \ z) in I ; :: thesis: I is associative-ideal of X

A5: for x, y, z being Element of X st (x \ y) \ z in I & y \ 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) \ z in I & y \ z in I implies x in I )

assume that

A6: (x \ y) \ z in I and

A7: y \ z in I ; :: thesis: x in I

x \ (y \ z) in I by A4, A6;

hence x in I by A7, BCIALG_1:def 18; :: thesis: verum

end;assume that

A6: (x \ y) \ z in I and

A7: y \ z in I ; :: thesis: x in I

x \ (y \ z) in I by A4, A6;

hence x in I by A7, BCIALG_1:def 18; :: thesis: verum

hence I is associative-ideal of X by A5, Def4; :: thesis: verum