let X be BCI-algebra; :: thesis: for x being Element of X holds x ` in AtomSet X
let x be Element of X; :: thesis: x ` in AtomSet X
0. X in AtomSet X by Th23;
hence x ` in AtomSet X by Th33; :: thesis: verum