let X be BCI-algebra; :: thesis: the carrier of X is closed Ideal of X
A1: the carrier of X is non empty Subset of X by ZFMISC_1:def 1;
A2: ( 0. X in the carrier of X & ( for x being Element of X holds x ` in the carrier of X ) ) ;
for x, y being Element of the carrier of X st x \ y in the carrier of X & y in the carrier of X holds
x in the carrier of X ;
hence the carrier of X is closed Ideal of X by A1, A2, Def18, Def19; :: thesis: verum