theorem Th28: :: BCIALG_1:28

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