let X be BCI-algebra; :: thesis: for x being Element of X ex a being Element of AtomSet X st a <= x
let x be Element of X; :: thesis: ex a being Element of AtomSet X st a <= x
take a = (x `) ` ; :: thesis: ( a is Element of AtomSet X & a <= x )
a \ x = 0. X by Th1;
hence ( a is Element of AtomSet X & a <= x ) by Th34; :: thesis: verum