let X be BCI-algebra; :: thesis: for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
let I be Ideal of X; :: thesis: ( I is associative-ideal of X implies for x being Element of X holds x \ ((0. X) \ x) in I )
assume A: I is associative-ideal of X ; :: thesis: for x being Element of X holds x \ ((0. X) \ x) in I
let x be Element of X; :: thesis: x \ ((0. X) \ x) in I
A1: 0. X in I by Def8, A;
x \ x = 0. X by BCIALG_1:def 5;
then (x \ (0. X)) \ x = 0. X by BCIALG_1:2;
hence x \ ((0. X) \ x) in I by A, TL31321, A1; :: thesis: verum