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