let X be BCI-algebra; :: thesis: {(0. X)} is closed Ideal of X
set X1 = {(0. X)};
reconsider X1 = {(0. X)} as Ideal of X by Lm3;
for x being Element of X1 holds x ` in X1 by Lm4;
hence {(0. X)} is closed Ideal of X by Def19; :: thesis: verum