let X be BCK-algebra; :: thesis: the carrier of X c= BCK-part X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of X or x in BCK-part X )
assume x in the carrier of X ; :: thesis: x in BCK-part X
then consider x1 being Element of X such that
A1: x = x1 ;
x1 ` = 0. X by BCIALG_1:def 8;
then 0. X <= x1 ;
hence x in BCK-part X by A1; :: thesis: verum