theorem :: BCIALG_1:26

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