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

proof

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;

0. X in X1 by A1, Def4;
hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum