:: deftheorem defines BCK-part BCIALG_1:def 12 :
for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ;