theorem Th31: :: BCIALG_1:31

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