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

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