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

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