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

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