for X being BCI-algebra st AtomSet X is Ideal of X holds
for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X