let X be BCI-algebra; :: thesis: for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds

I is closed Ideal of X

let I be Ideal of X; :: thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X )

assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; :: thesis: I is closed Ideal of X

for x1 being Element of I holds x1 ` in I

I is closed Ideal of X

let I be Ideal of X; :: thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X )

assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; :: thesis: I is closed Ideal of X

for x1 being Element of I holds x1 ` in I

proof

hence
I is closed Ideal of X
by BCIALG_1:def 19; :: thesis: verum
let x1 be Element of I; :: thesis: x1 ` in I

((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8;

then ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7;

then ((0. X) \ x1) \ x1 in I by A1;

hence x1 ` in I by BCIALG_1:def 18; :: thesis: verum

end;((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8;

then ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7;

then ((0. X) \ x1) \ x1 in I by A1;

hence x1 ` in I by BCIALG_1:def 18; :: thesis: verum