let X be BCI-algebra; :: thesis: for LC being L-congruence of X holds Class (LC,(0. X)) is closed Ideal of X

let LC be L-congruence of X; :: thesis: Class (LC,(0. X)) is closed Ideal of X

then 0. X in Class (LC,(0. X)) by EQREL_1:18;

then reconsider Rx = Class (LC,(0. X)) as Ideal of X by A1, BCIALG_1:def 18;

let LC be L-congruence of X; :: thesis: Class (LC,(0. X)) is closed Ideal of X

A1: now :: thesis: for x, y being Element of X st x \ y in Class (LC,(0. X)) & y in Class (LC,(0. X)) holds

x in Class (LC,(0. X))

[(0. X),(0. X)] in LC
by EQREL_1:5;x in Class (LC,(0. X))

let x, y be Element of X; :: thesis: ( x \ y in Class (LC,(0. X)) & y in Class (LC,(0. X)) implies x in Class (LC,(0. X)) )

assume that

A2: x \ y in Class (LC,(0. X)) and

A3: y in Class (LC,(0. X)) ; :: thesis: x in Class (LC,(0. X))

[(0. X),y] in LC by A3, EQREL_1:18;

then [(x \ (0. X)),(x \ y)] in LC by Def10;

then [x,(x \ y)] in LC by BCIALG_1:2;

then A4: [(x \ y),x] in LC by EQREL_1:6;

[(0. X),(x \ y)] in LC by A2, EQREL_1:18;

then [(0. X),x] in LC by A4, EQREL_1:7;

hence x in Class (LC,(0. X)) by EQREL_1:18; :: thesis: verum

end;assume that

A2: x \ y in Class (LC,(0. X)) and

A3: y in Class (LC,(0. X)) ; :: thesis: x in Class (LC,(0. X))

[(0. X),y] in LC by A3, EQREL_1:18;

then [(x \ (0. X)),(x \ y)] in LC by Def10;

then [x,(x \ y)] in LC by BCIALG_1:2;

then A4: [(x \ y),x] in LC by EQREL_1:6;

[(0. X),(x \ y)] in LC by A2, EQREL_1:18;

then [(0. X),x] in LC by A4, EQREL_1:7;

hence x in Class (LC,(0. X)) by EQREL_1:18; :: thesis: verum

then 0. X in Class (LC,(0. X)) by EQREL_1:18;

then reconsider Rx = Class (LC,(0. X)) as Ideal of X by A1, BCIALG_1:def 18;

now :: thesis: for x being Element of Rx holds x ` in Class (LC,(0. X))

hence
Class (LC,(0. X)) is closed Ideal of X
by BCIALG_1:def 19; :: thesis: verumlet x be Element of Rx; :: thesis: x ` in Class (LC,(0. X))

[(0. X),x] in LC by EQREL_1:18;

then [((0. X) `),(x `)] in LC by Def10;

then [(0. X),(x `)] in LC by BCIALG_1:def 5;

hence x ` in Class (LC,(0. X)) by EQREL_1:18; :: thesis: verum

end;[(0. X),x] in LC by EQREL_1:18;

then [((0. X) `),(x `)] in LC by Def10;

then [(0. X),(x `)] in LC by BCIALG_1:def 5;

hence x ` in Class (LC,(0. X)) by EQREL_1:18; :: thesis: verum