let X be BCI-algebra; :: thesis: X is SubAlgebra of X
A1: ( the carrier of X c= the carrier of X & 0. X = 0. X ) ;
dom the InternalDiff of X = [:the carrier of X,the carrier of X:] by FUNCT_2:def 1;
then the InternalDiff of X = the InternalDiff of X || the carrier of X by RELAT_1:97;
hence X is SubAlgebra of X by A1, Def10; :: thesis: verum