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

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