theorem :: BCIALG_1:25

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