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

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