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

proof

now

let xx be set ; :: 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;

hence {(0. X)} is Subset of X by TARSKI:def 3; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
set X1 = {(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;

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