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 )proof
assume A:
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 A1:
(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
by BCIALG_1:def 11;
then
(x \ (x \ y)) \ (y \ z) <= y \ (y \ z)
by BCIALG_1:5;
then A5:
((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z
by BCIALG_1:5;
C:
(y \ (y \ z)) \ z = 0. X
by BCIALG_1:1;
(((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X
by A5, C, BCIALG_1:def 11;
then
((x \ (x \ y)) \ (y \ z)) \ z = 0. X
by BCIALG_1:2;
then A8:
((x \ (x \ y)) \ (y \ z)) \ z in I
by Def8, A;
((x \ (y \ z)) \ (x \ y)) \ z in I
by A8, BCIALG_1:7;
hence
x \ (y \ z) in I
by Def8, A1, A;
:: thesis: verum
end;
assume B:
for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I
; :: thesis: I is associative-ideal of X
B1:
0. X in I
by BCIALG_1:def 18;
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 B1, Def8; :: thesis: verum