let X be BCI-algebra; :: thesis: for X1 being non empty Subset of X st X1 is associative-ideal of X holds

X1 is Ideal of X

let X1 be non empty Subset of X; :: thesis: ( X1 is associative-ideal of X implies X1 is Ideal of X )

assume A1: X1 is associative-ideal of X ; :: thesis: X1 is Ideal of X

A2: for x, y being Element of X st x \ y in X1 & y in X1 holds

x in X1

hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum

X1 is Ideal of X

let X1 be non empty Subset of X; :: thesis: ( X1 is associative-ideal of X implies X1 is Ideal of X )

assume A1: X1 is associative-ideal of X ; :: thesis: X1 is Ideal of X

A2: for x, y being Element of X st x \ y in X1 & y in X1 holds

x in X1

proof

0. X in X1
by A1, Def4;
let x, y be Element of X; :: thesis: ( x \ y in X1 & y in X1 implies x in X1 )

assume ( x \ y in X1 & y in X1 ) ; :: thesis: x in X1

then ( (x \ y) \ (0. X) in X1 & y \ (0. X) in X1 ) by BCIALG_1:2;

hence x in X1 by A1, Def4; :: thesis: verum

end;assume ( x \ y in X1 & y in X1 ) ; :: thesis: x in X1

then ( (x \ y) \ (0. X) in X1 & y \ (0. X) in X1 ) by BCIALG_1:2;

hence x in X1 by A1, Def4; :: thesis: verum

hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum