let X be BCI-algebra; :: thesis: {(0. X)} is Ideal of X
set X1 = {(0. X)};

now :: thesis: for xx being object st xx in {(0. X)} holds
xx in the carrier of X

let xx be object ; :: thesis: ( xx in {(0. X)} implies xx in the carrier of X )
assume xx in {(0. X)} ; :: thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def 1;
hence xx in the carrier of X ; :: thesis: verum

end;

then A1: {(0. X)} is Subset of X by TARSKI:def 3;
A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
x in {(0. X)}

proof

set X1 = {(0. X)};
let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;
then x = 0. X by Th2;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

0. X in {(0. X)} by TARSKI:def 1;
hence {(0. X)} is Ideal of X by A1, A2, Def18; :: thesis: verum