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