let X be BCK-algebra; :: thesis: BCK-part X = the carrier of X
the carrier of X c= BCK-part X by Lm1;
hence BCK-part X = the carrier of X by XBOOLE_0:def 10; :: thesis: verum