let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X
let a be Element of AtomSet X; :: thesis: for x being Element of X holds a \ x in AtomSet X
let x be Element of X; :: thesis: a \ x in AtomSet X
((a \ x) `) ` = a \ x by Th31;
hence a \ x in AtomSet X by Th29; :: thesis: verum