let X be BCI-algebra; :: thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
let x be Element of X; :: thesis: ( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
thus ( x in AtomSet X implies for z being Element of X holds z \ (z \ x) = x ) :: thesis: ( ( for z being Element of X holds z \ (z \ x) = x ) implies x in AtomSet X )

proof

assume A1: x in AtomSet X ; :: thesis: for z being Element of X holds z \ (z \ x) = x
let z be Element of X; :: thesis: z \ (z \ x) = x
consider x1 being Element of X such that
A2: ( x = x1 & x1 is atom ) by A1;
(z \ (z \ x)) \ x = 0. X by Th1;
hence z \ (z \ x) = x by A2, Def14; :: thesis: verum

end;

assume A3: for z being Element of X holds z \ (z \ x) = x ; :: thesis: x in AtomSet X

now

let z be Element of X; :: thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; :: thesis: z = x
then z \ (0. X) = x by A3;
hence z = x by Th2; :: thesis: verum

end;

then x is atom by Def14;
hence x in AtomSet X ; :: thesis: verum