theorem :: BCIALG_1:32

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )