let X be BCI-algebra; :: thesis: X is SubAlgebra of X

dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def 1;

then ( 0. X = 0. X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) ;

hence X is SubAlgebra of X by Def10; :: thesis: verum

dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def 1;

then ( 0. X = 0. X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) ;

hence X is SubAlgebra of X by Def10; :: thesis: verum