for X being BCK-algebra holds BCK-part X = the carrier of X by Lm1;