let X be BCI-algebra; :: thesis: 0. X in BCK-part X
(0. X) ` = 0. X by Def5;
then 0. X <= 0. X ;
hence 0. X in BCK-part X ; :: thesis: verum