theorem :: BCIIDEAL:11

for X being BCK-algebra
for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )