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 A1: 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
x \ x = 0. X by BCIALG_1:def 5;
then A2: (x \ (0. X)) \ x = 0. X by BCIALG_1:2;
0. X in I by A1, Def4;
hence x \ ((0. X) \ x) in I by A1, A2, Th15; :: thesis: verum